Segmentation failure

[LeventErkok]

This is on a Mac, with z3 compiled on March 28th from master.

The following program is "bad" since transitive-closure is given an integer instead of the name of an existing relation. I was expecting to get a syntax-error or some other kind of failure, but instead the program causes segmentation fault:

(declare-sort U 0)
(declare-fun R (U U) Bool)
(assert (forall ((x U) (y U)) (= (R x y) ((_ transitive-closure 0) x y))))
(declare-fun a () U)
(assert (not (R a a)))
(check-sat)

I get:

libc++abi: terminating due to uncaught exception of type std::bad_variant_access: bad_variant_access