Hi,
For this formula:
(declare-fun a () (_ BitVec 1))
(declare-fun b ((_ BitVec 1)) (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(assert (= (b (_ bv1 1)) c))
(assert (distinct (b a) c))
(check-sat-using qfufbv_ackr)
(get-model)
Z3 gives an invalid model:
sat
(model
(define-fun a () (_ BitVec 1)
#b1)
(define-fun c () (_ BitVec 1)
#b0)
(define-fun b ((x!0 (_ BitVec 1))) (_ BitVec 1)
#b0)
)
z3 incorrect model from the qfufbv_ackr tactic (the model clearly violates the second assert)
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: a319f4b
Hi,
For this formula:
Z3 gives an invalid model:
z3 incorrect model from the qfufbv_ackr tactic (the model clearly violates the second assert)
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: a319f4b