Hi,
For this formula:
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (not (exists ((e Real)) (=> (and (= 0 (/ a (- b e)) c)) (< c d)))))
(check-sat)
Z3 debug branch throws out a segmentation fault:
$ z3debug/build/z3 small.smt2
Segmentation fault
$ cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (not (exists ((e Real)) (=> (and (= 0 (/ a (- b e)) c)) (< c d)))))
(check-sat)
OS: Ubuntu 18.04
Commit: ceb2849
Hi,
For this formula:
Z3 debug branch throws out a segmentation fault:
OS: Ubuntu 18.04
Commit: ceb2849