(set-logic QF_ABV)
(set-info :status sat)
(declare-const v0 (_ BitVec 1))
(declare-const v1 (_ BitVec 15))
(declare-const v2 (_ BitVec 2))
(declare-const a0 (Array (_ BitVec 13) (_ BitVec 13) ))
(declare-const a1 (Array (_ BitVec 8) (_ BitVec 15) ))
(declare-const v3 (_ BitVec 8))
(declare-const v4 (_ BitVec 15))
(declare-const v5 (_ BitVec 8))
(declare-const v6 (_ BitVec 8))
(declare-const v7 (_ BitVec 13))
(declare-const v8 (_ BitVec 13))
(declare-const v9 (_ BitVec 13))
(declare-const v10 (_ BitVec 13))
(declare-const v11 (_ BitVec 15))
(assert (= #b1 (bvnot (ite (= (bvnot (ite (= (_ bv0 1) (bvnot (ite (bvult (bvmul (bvnot (_ bv0 15)) (ite (= v0 #b1) v1 (concat v2 (select (store (store a0 ((_ extract 12 0) (select (store (store a1 v3 v4) v5 v4) v6)) v7) v8 (select (store a0 ((_ extract 12 0) (select (store (store a1 v3 v4) v5 v4) v6)) v7) v9)) v10)))) v11) #b1 #b0))) #b1 #b0)) (bvnot (_ bv0 1))) #b1 #b0))))
(check-sat)