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