segmentation fault in recAddDefinition

[pcarbonn]

The following program results in a segmentation fault with Z3 4.8.12.0:

from z3 import *

f = Function('f', IntSort(), IntSort())
n = Int('n')
RecAddDefinition(f, n, If(n == 0, 1, 2))

A workaround is to use RecFunction (instead of Function) to declare f, even though it is not recursive. A possible fix would be to add an addFunction to the API, for non-recursive functions.

[NikolajBjorner]

Fixed the crash with an exception and a message.
Use RecFunction when a function is later going to be used in a recursive function definition.