Hi,
For this formula:
(set-logic NRA)
(assert
(exists ((a Real))
(forall ((b Real))
(exists ((c Real))
(and
(< (+ a (* 2 c)) 0)
(or (not (= a 0)) (< b 0))
(not (= (+ b c) 0))
(> c 0)
)
)
)
)
)
(check-sat)
Z3 latest version will hang on it:
$ timeout -s 9 120 z3 test.smt2
Killed
OS: Ubuntu 18.04
Revision: 0c972b8
Hi,
For this formula:
Z3 latest version will hang on it:
OS: Ubuntu 18.04
Revision: 0c972b8