(set-logic QF_ABV)
(set-info :status sat)
(declare-const a0 (Array (_ BitVec 3) (_ BitVec 3) ))
(declare-const v0 (_ BitVec 3))
(declare-const a1 (Array (_ BitVec 2) (_ BitVec 4) ))
(declare-const v1 (_ BitVec 2))
(declare-const v2 (_ BitVec 1))
(assert (= #b1 (ite (= (_ bv0 1) (bvand (ite (= (_ bv0 3) (select (store a0 (_ bv0 3) (concat (_ bv0 2) ((_ extract 1 1) v0))) (_ bv0 3))) #b1 #b0) (ite (= (_ bv0 1) (ite (= (_ bv0 4) (select (store (store (store a1 (concat (_ bv0 1) (ite (= (_ bv0 3) v0) #b1 #b0)) (_ bv0 4)) (_ bv0 2) (concat (_ bv0 3) ((_ extract 2 2) v0))) (concat (_ bv0 1) ((_ extract 0 0) (ite (= (ite (= (bvnot (_ bv0 1)) (ite (= v1 (concat (_ bv0 1) v2)) #b1 #b0)) #b1 #b0) #b1) (_ bv0 4) (concat (_ bv0 3) (ite (= (_ bv0 3) v0) #b1 #b0))))) (_ bv0 4)) (_ bv0 2))) #b1 #b0)) #b1 #b0))) #b1 #b0)))
(check-sat)