Hi,
the below log shows a soundness bug in Z3's debug build when running z3 with two threads.
[971] % z3 bug.smt2
sat
[972] % z3debug bug.smt2
sat
[973] % z3 smt.threads=2 bug.smt2
sat
[974] % z3debug smt.threads=2 bug.smt2
unsat
[975] % cat bug.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (not (exists ((d Real)) (xor (<= 0 d a) (= (mod (to_int d) (to_int c)) 1)
(= c (div 1 (to_int b)))))))
(check-sat)
OS: Ubuntu 18.04
Commit: bb63721
Hi,
the below log shows a soundness bug in Z3's debug build when running z3 with two threads.
OS: Ubuntu 18.04
Commit: bb63721