Hi,
For this formula,
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun f (Real) Real)
(declare-fun g (Real) Real)
(assert (= x (f x) y))
(assert (distinct (g x) (g y)))
(check-sat)
(get-model)
Z3 smt.arith.solver=1 incorrectly reports sat and gives an incorrect model:
(model
(define-fun x () Real
0.0)
(define-fun y () Real
0.0)
(define-fun f ((x!0 Real)) Real
0.0)
(define-fun g ((x!0 Real)) Real
(- 1.0))
)
OS: Ubuntu 18.04
Revision: e5ca451
Hi,
For this formula,
Z3 smt.arith.solver=1incorrectly reportssatand gives an incorrect model:OS: Ubuntu 18.04
Revision: e5ca451