(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(assert
(and
(> 0 (- d f))
(= d (ite (>= (/ a c) f) (+ b f) f))
(> 0 (/ a (/ c e)))
(or (= e 1.0) (= e 2.0))
(> d 0)
(= c 0)
)
)
(check-sat)
For this formula, Z3 reports sat, while CVC4 reports unsat,.
Z3 gives the following model:
(model
(define-fun e () Real 1.0)
(define-fun f () Real 2.0)
(define-fun a () Real 1.0)
(define-fun b () Real (- 1.0))
(define-fun c () Real 0.0)
(define-fun d () Real 1.0)
)
If I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Reversion: 5de35d4
For this formula, Z3 reports
sat, while CVC4 reportsunsat,.Z3 gives the following model:
If I feed this model to the formula, Z3 reports
unsat.OS: Ubuntu 18.04
Reversion: 5de35d4