Hi,
For this formula:
(set-option :proof true)
(assert (forall ((a Real) (b Real))
(or (>= (+ a b) (- 10 0))
(not (<= (+ (* a b)) 0))
(>= (+ (mod 0 b)) 3))))
(check-sat)
Z3 debug branch throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/smt/smt_conflict_resolution.cpp
Line: 811
(fact->get_arg(0) == n1->get_owner() && fact->get_arg(1) == n2->get_owner()) || (fact->get_arg(1) == n1->get_owner() && fact->get_arg(0) == n2->get_owner())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Commit: 3ac9dbd
Hi,
For this formula:
Z3 debug branch throws out an assertion violation:
OS: Ubuntu 18.04
Commit: 3ac9dbd