Hi,
For this formula:
(declare-fun a () Real)
(declare-fun b () Real)
(assert (> (/ b b b (- a b) (- 4 b) (+ a b) (* a ) b (/ 0 b) (- b) 0 (div 0 b)) 0))
(check-sat)
Z3 debug branch throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/math/lp/emonics.cpp
Line: 221
is_canonized(m)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Commit: d8d0b09
Hi,
For this formula:
Z3 debug branch throws out an assertion violation:
OS: Ubuntu 18.04
Commit: d8d0b09