Consider the following formula:
(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(assert (= (bvxnor a b c) (bvxnor (bvxnor a b) c)))
(check-sat)
Z3 reports unsat on it although the formula should clearly be sat.
OS: Ubuntu 18.04
Revision: 1fd4c91
Consider the following formula:
Z3 reports
unsaton it although the formula should clearly besat.OS: Ubuntu 18.04
Revision: 1fd4c91