stp_return_problem.smt2

(set-info :source | fuzzsmt 0.3 |)
(set-logic  QF_ABV)
(set-info :status unknown)
(declare-fun v0 () (_ BitVec 10))
(declare-fun v1 () (_ BitVec 4))
(declare-fun v2 () (_ BitVec 12))
(declare-fun v3 () (_ BitVec 8))
(declare-fun v4 () (_ BitVec 12))
(declare-fun a5 () (Array (_ BitVec 11) (_ BitVec 3)))
(declare-fun a6 () (Array (_ BitVec 2) (_ BitVec 3)))
(declare-fun a7 () (Array (_ BitVec 8) (_ BitVec 15)))
(assert
(let ((e8 (_ bv163 10)))
(let ((e9 (_ bv445 9)))
(let ((e10 (bvxnor ((_ sign_extend 6) v1) e8)))
(let ((e11 (bvxnor ((_ sign_extend 1) e9) v0)))
(let ((e12 (bvlshr v3 v3)))
(let ((e13 ((_ sign_extend 0) v2)))
(let ((e14 (ite (bvule v4 ((_ sign_extend 2) e8))(_ bv1 1) (_ bv0 1))))
(let ((e15 (store a6 ((_ extract 1 0) v1) ((_ extract 6 4) v2))))
(let ((e16 (store a6 ((_ extract 2 1) e12) ((_ extract 3 1) e8))))
(let ((e17 (store a6 ((_ extract 1 0) e12) ((_ extract 2 0) e8))))
(let ((e18 (select e17 ((_ extract 8 7) v4))))
(let ((e19 (select a6 ((_ extract 8 7) v0))))
(let ((e20 (store e15 ((_ extract 9 8) v0) ((_ zero_extend 2) e14))))
(let ((e21 (select a6 ((_ extract 1 0) e10))))
(let ((e22 (store a6 ((_ extract 1 0) v1) ((_ extract 2 0) e10))))
(let ((e23 (ite (bvule ((_ zero_extend 3) e9) v2)(_ bv1 1) (_ bv0 1))))
(let ((e24 ((_ rotate_right 2) v1)))
(let ((e25 (bvlshr ((_ sign_extend 2) e12) v0)))
(let ((e26 (bvor e14 e23)))
(let ((e27 (ite (bvult e23 e26)(_ bv1 1) (_ bv0 1))))
(let ((e28 ((_ extract 4 4) v3)))
(let ((e29 (bvnot v4)))
(let ((e30 (bvsrem ((_ sign_extend 9) e23) e11)))
(let ((e31 (ite (bvule e9 ((_ zero_extend 1) e12))(_ bv1 1) (_ bv0 1))))
(let ((e32 (ite (bvsgt e28 e31)(_ bv1 1) (_ bv0 1))))
(let ((e33 (ite (bvslt ((_ zero_extend 5) v1) e9)(_ bv1 1) (_ bv0 1))))
(let ((e34 (bvnot e21)))
(let ((e35 ((_ rotate_left 6) v3)))
(let ((e36 (bvsub e8 e10)))
(let ((e37 ((_ rotate_right 6) e9)))
(let ((e38 (bvmul ((_ sign_extend 9) e18) v4)))
(let ((e39 (bvudiv ((_ sign_extend 4) e35) v2)))
(let ((e40 (ite (bvslt ((_ sign_extend 5) e18) v3)(_ bv1 1) (_ bv0 1))))
(let ((e41 (bvxor e35 ((_ sign_extend 4) v1))))
(let ((e42 (bvsrem ((_ zero_extend 2) e40) e19)))
(let ((e43 ((_ sign_extend 2) e38)))
(let ((e44 (bvashr e13 ((_ sign_extend 11) e32))))
(let ((e45 (bvslt ((_ zero_extend 9) e31) v0)))
(let ((e46 (distinct ((_ sign_extend 2) v3) e10)))
(let ((e47 (distinct e41 ((_ zero_extend 4) v1))))
(let ((e48 (bvule e39 ((_ sign_extend 3) e37))))
(let ((e49 (bvsgt ((_ zero_extend 6) v1) e25)))
(let ((e50 (distinct e18 ((_ zero_extend 2) e33))))
(let ((e51 (bvugt e34 ((_ zero_extend 2) e32))))
(let ((e52 (bvsle e30 ((_ sign_extend 7) e19))))
(let ((e53 (bvule e38 ((_ zero_extend 4) v3))))
(let ((e54 (bvule ((_ zero_extend 4) v1) v3)))
(let ((e55 (bvsgt ((_ sign_extend 2) e12) e8)))
(let ((e56 (bvsle e8 e25)))
(let ((e57 (distinct e10 ((_ sign_extend 1) e9))))
(let ((e58 (bvuge v4 ((_ sign_extend 11) e27))))
(let ((e59 (bvsle ((_ zero_extend 2) e41) e36)))
(let ((e60 (bvsle ((_ zero_extend 7) e33) e12)))
(let ((e61 (distinct e42 e18)))
(let ((e62 (bvuge ((_ zero_extend 7) e23) v3)))
(let ((e63 (distinct e11 ((_ sign_extend 9) e31))))
(let ((e64 (bvule ((_ zero_extend 2) e25) e13)))
(let ((e65 (distinct e36 ((_ zero_extend 9) e32))))
(let ((e66 (bvsle e9 ((_ sign_extend 8) e23))))
(let ((e67 (bvslt ((_ zero_extend 2) e10) e39)))
(let ((e68 (bvsle ((_ zero_extend 3) e14) v1)))
(let ((e69 (bvult e31 e28)))
(let ((e70 (bvsge ((_ sign_extend 1) e42) e24)))
(let ((e71 (bvugt e44 e44)))
(let ((e72 (bvult ((_ sign_extend 9) e18) e38)))
(let ((e73 (bvugt e41 ((_ zero_extend 7) e26))))
(let ((e74 (bvule e37 ((_ sign_extend 8) e27))))
(let ((e75 (bvule v3 ((_ zero_extend 7) e28))))
(let ((e76 (bvult ((_ sign_extend 3) e9) e13)))
(let ((e77 (distinct ((_ zero_extend 9) e19) v2)))
(let ((e78 (distinct e34 ((_ sign_extend 2) e28))))
(let ((e79 (bvule e11 e25)))
(let ((e80 (bvuge v4 e44)))
(let ((e81 (bvult e38 ((_ zero_extend 8) e24))))
(let ((e82 (bvuge ((_ zero_extend 2) e25) v4)))
(let ((e83 (bvsle ((_ zero_extend 9) e18) e13)))
(let ((e84 (bvugt ((_ sign_extend 6) v1) e8)))
(let ((e85 (bvule e39 ((_ sign_extend 2) e11))))
(let ((e86 (bvule e10 ((_ sign_extend 7) e42))))
(let ((e87 (bvslt ((_ sign_extend 2) e28) e18)))
(let ((e88 (bvuge v4 ((_ sign_extend 2) e10))))
(let ((e89 (bvule e10 ((_ sign_extend 1) e9))))
(let ((e90 (bvuge ((_ zero_extend 9) e19) v2)))
(let ((e91 (bvsle e37 e9)))
(let ((e92 (bvuge ((_ sign_extend 7) e14) e35)))
(let ((e93 (bvule e42 e34)))
(let ((e94 (distinct e11 ((_ zero_extend 7) e42))))
(let ((e95 (bvule ((_ zero_extend 3) e33) e24)))
(let ((e96 (distinct v4 ((_ zero_extend 9) e42))))
(let ((e97 (bvsle e36 e11)))
(let ((e98 (bvsgt e25 ((_ sign_extend 7) e42))))
(let ((e99 (bvslt e12 ((_ zero_extend 7) e32))))
(let ((e100 (bvsgt e43 ((_ sign_extend 13) e32))))
(let ((e101 (bvsgt ((_ zero_extend 2) e35) e11)))
(let ((e102 (bvsle ((_ sign_extend 1) e41) e37)))
(let ((e103 (bvult ((_ zero_extend 9) e33) v0)))
(let ((e104 (bvule e21 ((_ sign_extend 2) e28))))
(let ((e105 (bvsgt ((_ zero_extend 2) e10) e44)))
(let ((e106 (bvult e13 ((_ zero_extend 4) e35))))
(let ((e107 (bvsle e33 e23)))
(let ((e108 (bvsgt e44 ((_ sign_extend 4) v3))))
(let ((e109 (bvsge ((_ sign_extend 4) v1) e12)))
(let ((e110 (= e9 ((_ sign_extend 8) e23))))
(let ((e111 (bvule ((_ sign_extend 5) v1) e9)))
(let ((e112 (bvsge ((_ sign_extend 1) e9) v0)))
(let ((e113 (bvult e32 e32)))
(let ((e114 (bvslt v4 ((_ sign_extend 2) e36))))
(let ((e115 (bvult ((_ zero_extend 1) e9) e36)))
(let ((e116 (bvuge e29 ((_ zero_extend 4) e41))))
(let ((e117 (bvsge e37 ((_ zero_extend 1) v3))))
(let ((e118 (bvuge ((_ sign_extend 6) e35) e43)))
(let ((e119 (= e8 ((_ zero_extend 9) e40))))
(let ((e120 (xor e91 e70)))
(let ((e121 (=> e116 e83)))
(let ((e122 (and e89 e113)))
(let ((e123 (=> e92 e106)))
(let ((e124 (=> e95 e45)))
(let ((e125 (=> e76 e108)))
(let ((e126 (ite e103 e72 e87)))
(let ((e127 (xor e100 e81)))
(let ((e128 (xor e105 e117)))
(let ((e129 (not e80)))
(let ((e130 (not e112)))
(let ((e131 (=> e102 e85)))
(let ((e132 (ite e66 e73 e60)))
(let ((e133 (or e125 e86)))
(let ((e134 (not e50)))
(let ((e135 (and e120 e129)))
(let ((e136 (=> e61 e104)))
(let ((e137 (=> e75 e52)))
(let ((e138 (= e134 e121)))
(let ((e139 (not e77)))
(let ((e140 (or e123 e65)))
(let ((e141 (ite e82 e97 e68)))
(let ((e142 (and e115 e69)))
(let ((e143 (ite e90 e56 e133)))
(let ((e144 (=> e135 e132)))
(let ((e145 (and e130 e107)))
(let ((e146 (or e145 e47)))
(let ((e147 (not e140)))
(let ((e148 (ite e141 e127 e138)))
(let ((e149 (or e46 e57)))
(let ((e150 (= e147 e144)))
(let ((e151 (ite e74 e101 e51)))
(let ((e152 (=> e131 e149)))
(let ((e153 (=> e53 e128)))
(let ((e154 (= e118 e126)))
(let ((e155 (xor e59 e152)))
(let ((e156 (xor e136 e64)))
(let ((e157 (ite e150 e153 e54)))
(let ((e158 (not e137)))
(let ((e159 (ite e154 e79 e154)))
(let ((e160 (ite e146 e159 e93)))
(let ((e161 (and e48 e71)))
(let ((e162 (=> e157 e94)))
(let ((e163 (ite e88 e99 e58)))
(let ((e164 (or e55 e78)))
(let ((e165 (xor e163 e111)))
(let ((e166 (and e67 e63)))
(let ((e167 (ite e160 e96 e160)))
(let ((e168 (xor e124 e165)))
(let ((e169 (or e166 e110)))
(let ((e170 (and e155 e142)))
(let ((e171 (xor e161 e62)))
(let ((e172 (=> e119 e98)))
(let ((e173 (=> e143 e172)))
(let ((e174 (ite e169 e164 e171)))
(let ((e175 (= e174 e162)))
(let ((e176 (not e114)))
(let ((e177 (or e151 e148)))
(let ((e178 (ite e49 e177 e175)))
(let ((e179 (=> e178 e173)))
(let ((e180 (=> e176 e84)))
(let ((e181 (ite e170 e168 e170)))
(let ((e182 (= e122 e181)))
(let ((e183 (not e182)))
(let ((e184 (=> e179 e109)))
(let ((e185 (and e180 e167)))
(let ((e186 (ite e184 e184 e185)))
(let ((e187 (not e158)))
(let ((e188 (ite e187 e183 e156)))
(let ((e189 (or e139 e139)))
(let ((e190 (=> e189 e186)))
(let ((e191 (or e188 e188)))
(let ((e192 (or e191 e191)))
(let ((e193 (= e192 e192)))
(let ((e194 (not e193)))
(let ((e195 (= e194 e190)))
(let ((e196 (and e195 (not (= v2 (_ bv0 12))))))
(let ((e197 (and e196 (not (= e19 (_ bv0 3))))))
(let ((e198 (and e197 (not (= e19 (bvnot (_ bv0 3)))))))
(let ((e199 (and e198 (not (= e11 (_ bv0 10))))))
(let ((e200 (and e199 (not (= e11 (bvnot (_ bv0 10)))))))
e200
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)