Hi,
For this formula:
(declare-fun a () Real)
(assert (forall ((b Real)) (> (/ 0 (* (- 2 (* a b)))) (/ 0 (- a b)))))
(check-sat-using qe_rec)
Z3 throws out an assertion violation:
Failed to verify: a.is_numeral(val, r)
ASSERTION VIOLATION
File: ../src/qe/qe_arith.cpp
Line: 348
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
OS: Ubuntu 18.04
Commit: a14c2a3
Hi,
For this formula:
Z3 throws out an assertion violation:
OS: Ubuntu 18.04
Commit: a14c2a3