Hi,
For this formula:
(declare-fun a () Int)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (>= a 4))
(assert (= (+ b (* b c)) 3.0))
(check-sat)
(check-sat)
(get-model)
Z3 gives an invalid model:
(model
(define-fun b () Real
(/ 1.0 8.0))
(define-fun c () Real
23.0)
(define-fun a () Int
0)
)
if I feed this model to the formula, Z3 reports unsat.
It may be related to #3049.
OS: Ubuntu 18.04
Commit: e8f7a08
Hi,
For this formula:
Z3 gives an invalid model:
if I feed this model to the formula, Z3 reports unsat.
It may be related to #3049.
OS: Ubuntu 18.04
Commit: e8f7a08