(declare-const v (_ BitVec 1))
(declare-const u (_ BitVec 1))
(declare-const i (_ BitVec 1))
(declare-const j (_ BitVec 1))
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (and (not (= i j)) (not (= u v)) (= (store (store a ((_ zero_extend 31) i) ((_ zero_extend 7) u)) ((_ zero_extend 31) j) (_ bv0 8)) (store a ((_ zero_extend 31) i) ((_ zero_extend 7) v)))))
(check-sat)
Z3 32beb91
Solution soundness