(set-logic QF_ABV)
(set-info :status sat)
(declare-const v0 (_ BitVec 24))
(declare-const a0 (Array (_ BitVec 32) (_ BitVec 8) ))
(declare-const v1 (_ BitVec 32))
(declare-const v2 (_ BitVec 32))
(declare-const v3 (_ BitVec 32))
(declare-const v4 (_ BitVec 32))
(declare-const v5 (_ BitVec 32))
(declare-const v6 (_ BitVec 32))
(declare-const v7 (_ BitVec 32))
(declare-const v8 (_ BitVec 32))
(declare-const v9 (_ BitVec 32))
(declare-const v10 (_ BitVec 32))
(declare-const v11 (_ BitVec 8))
(declare-const v12 (_ BitVec 32))
(declare-const v13 (_ BitVec 32))
(declare-const v14 (_ BitVec 32))
(declare-const v15 (_ BitVec 8))
(declare-const v16 (_ BitVec 32))
(declare-const v17 (_ BitVec 32))
(declare-const v18 (_ BitVec 32))
(declare-const v19 (_ BitVec 32))
(declare-const v20 (_ BitVec 8))
(declare-const v21 (_ BitVec 32))
(declare-const v22 (_ BitVec 32))
(declare-const v23 (_ BitVec 32))
(declare-const v24 (_ BitVec 32))
(declare-const v25 (_ BitVec 32))
(declare-const v26 (_ BitVec 32))
(declare-const v27 (_ BitVec 32))
(declare-const v28 (_ BitVec 32))
(declare-const v29 (_ BitVec 32))
(declare-const v30 (_ BitVec 32))
(declare-const v31 (_ BitVec 32))
(declare-const v32 (_ BitVec 32))
(declare-const v33 (_ BitVec 32))
(declare-const v34 (_ BitVec 32))
(declare-const v35 (_ BitVec 32))
(declare-const v36 (_ BitVec 32))
(declare-const v37 (_ BitVec 32))
(declare-const v38 (_ BitVec 32))
(declare-const v39 (_ BitVec 32))
(declare-const v40 (_ BitVec 32))
(declare-const v41 (_ BitVec 32))
(declare-const v42 (_ BitVec 32))
(declare-const v43 (_ BitVec 32))
(declare-const v44 (_ BitVec 32))
(declare-const v45 (_ BitVec 32))
(declare-const v46 (_ BitVec 32))
(declare-const v47 (_ BitVec 32))
(declare-const v48 (_ BitVec 32))
(declare-const v49 (_ BitVec 32))
(declare-const v50 (_ BitVec 32))
(declare-const v51 (_ BitVec 32))
(declare-const v52 (_ BitVec 32))
(declare-const v53 (_ BitVec 32))
(declare-const v54 (_ BitVec 32))
(declare-const v55 (_ BitVec 32))
(declare-const v56 (_ BitVec 32))
(assert (= #b1 (ite (= #b00000000000000000000000000000000 (concat v0 (select (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a0 v1 #b00000000) v2 #b00000000) v3 #b00000000) v4 #b00000000) v5 (bvnot #b00000000)) v6 #b00000000) v7 #b00000000) v8 #b00000000) v9 #b00000000) v10 v11) v12 (bvnot #b00000000)) v13 #b00000000) v14 v15) v16 v11) v17 v11) v18 v11) v19 v11) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v20) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) v21 #b00000000) v22 #b00000000) v23 #b00000000) v24 #b00000000) v25 #b00000000) v26 #b00000000) v27 #b00000000) v28 #b00000000) v29 #b00000000) v30 #b00000000) v31 #b00000000) v32 #b00000000) v33 #b00000000) v34 #b00000000) v35 #b00000000) v36 #b00000000) v37 #b00000000) v38 #b00000000) v39 #b00000000) v40 #b00000000) v41 #b00000000) v42 v11) v43 v11) v44 v11) v45 #b00000000) v46 #b00000000) v47 #b00000000) v48 #b00000000) v49 #b00000000) v50 v11) v51 v11) v52 v11) v53 #b00000000) v54 #b00000000) v55 #b00000000) v56 #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) ((_ extract 31 24) (bvnot (concat #b000000000000000000000000 (select (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a0 v1 #b00000000) v2 #b00000000) v3 #b00000000) v4 #b00000000) v5 (bvnot #b00000000)) v6 #b00000000) v7 #b00000000) v8 #b00000000) v9 #b00000000) v10 v11) v12 (bvnot #b00000000)) v13 #b00000000) v14 v15) v16 v11) v17 v11) v18 v11) v19 v11) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v20) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) (bvnot #b00000000000000000000000000000000) v11) v21 #b00000000) v22 #b00000000) v23 #b00000000) v24 #b00000000) v25 #b00000000) v26 #b00000000) v27 #b00000000) v28 #b00000000) v29 #b00000000) v30 #b00000000) v31 #b00000000) v32 #b00000000) v33 #b00000000) v34 #b00000000) v35 #b00000000) v36 #b00000000) v37 #b00000000) v38 #b00000000) v39 #b00000000) v40 #b00000000) v41 #b00000000) v42 v11) v43 v11) v44 v11) v45 #b00000000) v46 #b00000000) v47 #b00000000) v48 #b00000000) v49 #b00000000) v50 v11) v51 v11) v52 v11) v53 #b00000000) v54 #b00000000) v55 #b00000000) v56 #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) (bvnot #b00000000000000000000000000000000) #b00000000) v49))))) v1))) #b1 #b0)))
(check-sat)