Debug branch: Soundness bug on QF_NRA formula #3263
Description
Hi,
For this formula:
( declare-fun a () Real )
( declare-fun b () Real )
( declare-fun c () Real )
( declare-fun d () Real )
( declare-fun e () Real )
( declare-fun f () Real )
( declare-fun g () Real )
( declare-fun h () Real )
( declare-fun i () Real )
(assert (not (=> (and (= (- b e ) g) (< 0 (- b e ))
(< (+ g (/ 0 (* 2.0 (- a d )))) 0)) (< 0.0 (- a d)) (<= 0 h ))))
(assert ( = c ( mod f i )))
(check-sat)
Z3 debug branch gives an incorrect answer:
$ z3/build/z3 small.smt2
unsat
$ z3debug/build/z3 small.smt2
sat
$ cat small.smt2
( declare-fun a () Real )
( declare-fun b () Real )
( declare-fun c () Real )
( declare-fun d () Real )
( declare-fun e () Real )
( declare-fun f () Real )
( declare-fun g () Real )
( declare-fun h () Real )
( declare-fun i () Real )
(assert (not (=> (and (= (- b e ) g) (< 0 (- b e ))
(< (+ g (/ 0 (* 2.0 (- a d )))) 0)) (< 0.0 (- a d)) (<= 0 h ))))
(assert ( = c ( mod f i )))
(check-sat)
OS: Ubuntu 18.04
Commit: a02d3e9