(set-info :status unsat)
(declare-fun r () (Array (_ BitVec 4) (_ BitVec 4)))
(assert (= r (store r (_ bv0 4) (_ bv0 4))))
(assert (= (_ bv1 4) (select r (_ bv0 4))))
(check-sat)