Hi,
For this formula,
(declare-fun a () Int)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)
(assert (= b (= (/ 1 0) a) (= b d e) (= e c d)))
(check-sat)
(get-model)
z3 will report a invaild model:
(model
(define-fun e () Bool
true)
(define-fun c () Bool
false)
(define-fun d () Bool
true)
(define-fun a () Int
0)
(define-fun b () Bool
true)
)
OS: Ubuntu 18.04
Revision: 16d4ccd
Hi,
For this formula,
z3 will report a invaild model:
OS: Ubuntu 18.04
Revision: 16d4ccd