Hi,
For this case, Z3 gives an incorrect answer:
[548] % z3 small.smt2
sat
unsat
[549] %
[549] % cat small.smt2
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(assert (forall ((c (_ BitVec 1))) (distinct (bvor c a) b)))
(check-sat)
(check-sat-using qe_rec)
[550] %
OS: Ubuntu 18.04
Commit: 164a73f
Hi,
For this case, Z3 gives an incorrect answer:
OS: Ubuntu 18.04
Commit: 164a73f