Consider the below trace which shows a soundness bug on a NRA formula. Z3 (master + debug) return sat, CVC4 gives unsat on bug.smt2. Feeding Z3's model to the formula yields unsat.
No related issues: I have scanned the other open "soundness bug issues". None of those has the following characteristics (1) NRA, (2) master + debug branch (3) no options.
% z3-8717c7d bug.smt2
sat
% z3debug-8d39694 bug.smt2
sat
% cvc4 bug.smt2
unsat
% cat bug.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun v () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun w () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun ep () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun s () Real)
(assert (not (exists ((t Real)) (= (and (and (and (= l 0.0))
(< (+ g (/ (/ (- a m) m) (* 2.0 (+ b r)))) h))
(<= a (- 6 d (- v ep ))))
(or (= (= (<= 0.0 t) (and (<= l (* d (- v ep))) (<= 0 ep))) (= j 2.0)))))))
(assert (not (exists ((u Real)) (=> (= 0.0 (* ( / 91 i ) q e k))
(= (- c w) 2.0) (= o 2.0)))))
(assert (= c (+ w p ) v (+ ep p)))
(assert (= f (/ l s)))
(check-sat)
OS: Ubuntu 18.04
Commit: 8d39694 (master) + 8d39694 (debug)
Consider the below trace which shows a soundness bug on a NRA formula. Z3 (master + debug) return
sat, CVC4 givesunsaton bug.smt2. Feeding Z3's model to the formula yieldsunsat.No related issues: I have scanned the other open "soundness bug issues". None of those has the following characteristics (1) NRA, (2) master + debug branch (3) no options.
OS: Ubuntu 18.04
Commit: 8d39694 (master) + 8d39694 (debug)