(set-logic QF_ABV)
(set-info :status unsat)
(declare-const a0 (Array (_ BitVec 1) (_ BitVec 1) ))
(assert (= #b1 (select (store a0 (ite (= a0 (store a0 #b0 #b0)) #b1 #b0) #b0) #b0)))
(check-sat)