; COMMAND-LINE: -q --check-unsat-cores --check-models
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun c () (_ BitVec 32))
(declare-fun d () (_ BitVec 32))
(declare-fun e () (_ BitVec 32))
(declare-fun f () (_ BitVec 32))
(declare-fun g () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= (= d e) (= (select a c) f)))
(assert (= g (store b (bvxor (_ bv4 32) f) (_ bv0 32))))
(check-sat)