Hi,
Here is a QF_NRA crash case.
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (or (= c 0) (> (* 2 (/ a b)) 0)))
(assert (= b (/ a d) d (/ a b)))
(check-sat)
ASSERTION VIOLATION
File: ../src/nlsat/nlsat_solver.cpp
Line: 1154
value(l) == l_undef
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Revision: 0b06a9b
OS: Ubuntu 18.04
Hi,
Here is a QF_NRA crash case.
Revision: 0b06a9b
OS: Ubuntu 18.04