This formula should be unsat, while Z3 gives an incorrect sat:
[633] % cvc4 -q small.smt2
unsat
[634] % z3release small.smt2
sat
[635] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (_ BitVec 32))
(assert
(distinct
(store
(store
(store a b (select a (bvsdiv b (_ bv1 32))))
(bvor b (_ bv1 32))
(select a (bvadd b (_ bv1 32))))
b
(select a b))
a))
(check-sat)
[636] %
OS: Ubuntu 18.04
Commit: 49a0266
This formula should be unsat, while Z3 gives an incorrect sat:
OS: Ubuntu 18.04
Commit: 49a0266