Hi,
For this formula,
(declare-fun a () Real)
(declare-fun b (Real) Real)
(assert (distinct (b a) (/ 0 a)))
(check-sat)
Z3 smt.arith.solver=1 throws out an assertion violation:
(smt.diff_logic: non-diff logic expression (/ 0.0 a))
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 771
e_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Revision: 7b0327d
Hi,
For this formula,
Z3 smt.arith.solver=1throws out an assertion violation:OS: Ubuntu 18.04
Revision: 7b0327d