(define-fun A0 () (Array (_ BitVec 2) (_ BitVec 2)) ((as const (Array (_ BitVec 2) (_ BitVec 2))) #b00))
(define-fun A00 () (Array (_ BitVec 2) (Array (_ BitVec 2) (_ BitVec 2))) ((as const (Array (_ BitVec 2) (Array (_ BitVec 2) (_ BitVec 2)))) A0))
(push 1)
(assert (not (= #b00 (select (select (store A00 #b00 A0) #b01) #b00))))
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert (not (= #b01 (select (select (store A00 #b00 A0) #b00) #b00))))
(set-info :status sat)
(check-sat)
(pop 1)