Hi
consider the following formula.
(set-logic QF_NRA)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert
(let ((d 0)) (let ((e 0))
(distinct true (= true (= 0 a))
(distinct true (not (<= c 0))
(= false (distinct false
(distinct false (= a b)))))))))
(check-sat)
Z3 reports sat on it but feeding the model to it yields unsat.
The bug should have been introduced one commit after 6ad55cc or later.
Z3 (revision 6ad55cc) correctly returns unsat
OS: Ubuntu 18.04
Revision: 78feac4
Hi
consider the following formula.
Z3 reports
saton it but feeding the model to it yieldsunsat.The bug should have been introduced one commit after
6ad55ccor later.Z3 (revision 6ad55cc) correctly returns unsat
OS: Ubuntu 18.04
Revision: 78feac4