(benchmark fuzzsmt
:logic QF_AUFBV
:status sat
:extrafuns ((v0 BitVec[15]))
:extrafuns ((v1 BitVec[3]))
:extrafuns ((v2 BitVec[11]))
:extrafuns ((a3 Array[3:5]))
:extrafuns ((a4 Array[5:15]))
:extrafuns ((a5 Array[2:13]))
:extrafuns ((a6 Array[1:13]))
:extrafuns ((a7 Array[3:7]))
:extrafuns ((a8 Array[4:14]))
:extrafuns ((a9 Array[8:5]))
:extrafuns ((a10 Array[3:14]))
:formula
(let (?e11 bv1572[12])
(let (?e12 bv33[9])
(let (?e13 bv33[6])
(let (?e14 bv18[7])
(let (?e15 bv19308[16])
(let (?e16 bv1[1])
(let (?e17 bv13[4])
(let (?e18 (bvlshr (zero_extend[7] ?e17) v2))
(let (?e19 (ite (= bv1[1] (extract[4:4] ?e12)) ?e15 (sign_extend[9] ?e14)))
(let (?e20 (ite (bvugt ?e12 (zero_extend[8] ?e16)) bv1[1] bv0[1]))
(let (?e21 (bvnor (zero_extend[8] v1) v2))
(let (?e22 (bvnot ?e21))
(let (?e23 (ite (bvsge (sign_extend[5] ?e13) v2) bv1[1] bv0[1]))
(let (?e24 (ite (bvsge ?e11 (zero_extend[1] ?e22)) bv1[1] bv0[1]))
(let (?e25 (ite (bvsle v0 (sign_extend[4] v2)) bv1[1] bv0[1]))
(let (?e26 (store a9 (extract[9:2] ?e21) (extract[5:1] ?e18)))
(let (?e27 (store a6 (extract[0:0] ?e22) (sign_extend[10] v1)))
(let (?e28 (store a6 (extract[2:2] v1) (zero_extend[12] ?e24)))
(let (?e29 (store a9 (extract[7:0] ?e22) (extract[8:4] v0)))
(let (?e30 (store a10 (extract[7:5] ?e22) (zero_extend[10] ?e17)))
(let (?e31 (ite (= a8 a8) bv1[1] bv0[1]))
(let (?e32 (select ?e28 ?e16))
(let (?e33 (select ?e29 (extract[13:6] ?e15)))
(let (?e34 (select a3 (zero_extend[2] ?e23)))
(let (?e35 (select ?e30 (zero_extend[2] ?e20)))
(let (?e36 (select a5 (sign_extend[1] ?e20)))
(let (?e37 (select a4 (sign_extend[4] ?e24)))
(let (?e38 (select ?e26 (zero_extend[7] ?e31)))
(let (?e39 (store a6 ?e16 (zero_extend[8] ?e33)))
(let (?e40 (store a7 (extract[7:5] ?e15) (zero_extend[6] ?e16)))
(let (?e41 (store a9 (extract[8:1] ?e21) ?e38))
(let (?e42 (select a3 (zero_extend[2] ?e23)))
(let (?e43 (select a4 (extract[6:2] ?e22)))
(let (?e44 (select a4 (extract[5:1] ?e13)))
(let (?e45 (store ?e30 (extract[4:2] ?e42) (sign_extend[5] ?e12)))
(let (?e46 (select ?e39 (extract[0:0] ?e22)))
(let (?e47 (select ?e40 (extract[2:0] ?e14)))
(let (?e48 (store ?e28 (extract[0:0] ?e18) ?e46))
(let (?e49 (select ?e40 (extract[5:3] v2)))
(let (?e50 (bvxor (zero_extend[8] ?e34) ?e46))
(let (?e51 (bvneg ?e49))
(let (?e52 (ite (bvsge (zero_extend[4] ?e21) ?e44) bv1[1] bv0[1]))
(let (?e53 (ite (bvuge ?e12 (zero_extend[2] ?e51)) bv1[1] bv0[1]))
(let (?e54 (bvor ?e32 (zero_extend[12] ?e53)))
(let (?e55 (repeat[10] ?e23))
(let (?e56 (bvnot ?e13))
(let (?e57 (rotate_right[0] ?e23))
(let (?e58 (ite (bvsge ?e35 (sign_extend[1] ?e46)) bv1[1] bv0[1]))
(let (?e59 (bvxor ?e47 ?e47))
(let (?e60 (sign_extend[2] ?e18))
(let (?e61 (rotate_right[2] v1))
(let (?e62 (bvadd (zero_extend[2] ?e36) ?e44))
(let (?e63 (bvand ?e25 ?e53))
(let (?e64 (bvneg ?e19))
(let (?e65 (extract[8:2] ?e22))
(let (?e66 (rotate_right[0] ?e16))
(let (?e67 (bvlshr (zero_extend[11] v1) ?e35))
(let (?e68 (zero_extend[7] ?e59))
(let (?e69 (ite (bvsle ?e22 (sign_extend[10] ?e20)) bv1[1] bv0[1]))
(let (?e70 (rotate_right[4] ?e55))
(let (?e71 (bvshl v0 (sign_extend[8] ?e51)))
(let (?e72 (bvshl ?e33 (sign_extend[4] ?e31)))
(let (?e73 (bvxor ?e19 (sign_extend[15] ?e52)))
(let (?e74 (bvnor (sign_extend[13] ?e31) ?e68))
(let (?e75 (extract[0:0] ?e24))
(let (?e76 (ite (= bv1[1] (extract[6:6] ?e71)) (zero_extend[4] ?e23) ?e42))
(let (?e77 (bvand (sign_extend[1] ?e37) ?e15))
(let (?e78 (bvashr ?e43 ?e62))
(let (?e79 (repeat[1] ?e15))
(let (?e80 (ite (bvule (sign_extend[8] ?e14) v0) bv1[1] bv0[1]))
(let (?e81 (ite (bvslt (zero_extend[10] v1) ?e54) bv1[1] bv0[1]))
(let (?e82 (ite (= (sign_extend[6] ?e38) ?e18) bv1[1] bv0[1]))
(let (?e83 (ite (bvsgt (zero_extend[8] ?e56) ?e67) bv1[1] bv0[1]))
(let (?e84 (bvmul ?e32 (sign_extend[2] ?e22)))
(let (?e85 (extract[7:6] ?e11))
(let (?e86 (repeat[1] ?e55))
(let (?e87 (bvashr (sign_extend[2] ?e54) ?e62))
(let (?e88 (rotate_left[1] ?e55))
(let (?e89 (concat ?e83 ?e69))
(let (?e90 (bvadd (zero_extend[5] v2) ?e15))
(let (?e91 (bvor ?e22 (sign_extend[8] ?e61)))
(let (?e92 (extract[12:10] ?e79))
(let (?e93 (ite (bvslt (zero_extend[14] ?e83) ?e62) bv1[1] bv0[1]))
(let (?e94 (ite (bvsgt (sign_extend[9] ?e17) ?e60) bv1[1] bv0[1]))
(flet ($e95 (bvugt (sign_extend[8] v1) v2))
(flet ($e96 (bvult (sign_extend[1] ?e87) ?e19))
(flet ($e97 (bvule ?e47 (zero_extend[5] ?e85)))
(flet ($e98 (bvsge ?e68 (sign_extend[7] ?e59)))
(flet ($e99 (bvuge ?e51 (sign_extend[2] ?e38)))
(flet ($e100 (bvule (zero_extend[11] ?e42) ?e73))
(flet ($e101 (bvuge ?e87 (sign_extend[2] ?e32)))
(flet ($e102 (distinct ?e47 (zero_extend[1] ?e56)))
(flet ($e103 (distinct ?e32 (sign_extend[4] ?e12)))
(flet ($e104 (bvuge (sign_extend[6] ?e69) ?e47))
(flet ($e105 (bvsle ?e59 (zero_extend[6] ?e52)))
(flet ($e106 (bvsgt ?e67 (zero_extend[8] ?e56)))
(flet ($e107 (bvsle (zero_extend[2] ?e93) ?e92))
(flet ($e108 (bvuge ?e72 (zero_extend[4] ?e81)))
(flet ($e109 (bvult (zero_extend[13] ?e57) ?e35))
(flet ($e110 (bvsge ?e74 (sign_extend[13] ?e69)))
(flet ($e111 (bvslt ?e68 (sign_extend[8] ?e13)))
(flet ($e112 (bvslt (sign_extend[4] ?e69) ?e38))
(flet ($e113 (bvsle (zero_extend[3] ?e36) ?e79))
(flet ($e114 (bvule ?e51 (zero_extend[6] ?e23)))
(flet ($e115 (bvsle (sign_extend[7] ?e85) ?e12))
(flet ($e116 (bvsge (sign_extend[2] ?e31) ?e61))
(flet ($e117 (bvugt ?e77 (sign_extend[11] ?e76)))
(flet ($e118 (bvsge (sign_extend[11] ?e85) ?e46))
(flet ($e119 (= (sign_extend[9] ?e25) ?e70))
(flet ($e120 (bvsge ?e47 (zero_extend[6] ?e52)))
(flet ($e121 (= (sign_extend[7] ?e51) ?e35))
(flet ($e122 (= ?e78 (zero_extend[8] ?e14)))
(flet ($e123 (bvslt (zero_extend[4] ?e91) ?e87))
(flet ($e124 (bvslt (sign_extend[12] ?e92) ?e44))
(flet ($e125 (distinct ?e58 ?e80))
(flet ($e126 (bvugt ?e53 ?e58))
(flet ($e127 (bvsgt (sign_extend[5] ?e88) ?e87))
(flet ($e128 (bvslt ?e37 v0))
(flet ($e129 (bvsge (zero_extend[2] ?e23) v1))
(flet ($e130 (bvule ?e50 ?e36))
(flet ($e131 (bvsgt (zero_extend[13] ?e92) ?e73))
(flet ($e132 (bvult (zero_extend[10] ?e72) ?e37))
(flet ($e133 (bvsle ?e93 ?e53))
(flet ($e134 (bvsge (sign_extend[2] ?e91) ?e46))
(flet ($e135 (bvuge (sign_extend[13] ?e52) ?e67))
(flet ($e136 (bvsge (sign_extend[13] ?e23) ?e67))
(flet ($e137 (bvslt ?e70 (sign_extend[9] ?e69)))
(flet ($e138 (bvult ?e88 ?e55))
(flet ($e139 (bvsle ?e87 ?e78))
(flet ($e140 (bvsle ?e62 (zero_extend[14] ?e83)))
(flet ($e141 (bvugt ?e67 (zero_extend[13] ?e69)))
(flet ($e142 (= ?e71 (zero_extend[2] ?e46)))
(flet ($e143 (bvslt (zero_extend[9] ?e34) ?e67))
(flet ($e144 (bvsge ?e14 ?e51))
(flet ($e145 (bvult ?e51 (sign_extend[2] ?e33)))
(flet ($e146 (bvugt (zero_extend[9] ?e25) ?e70))
(flet ($e147 (bvule ?e64 (sign_extend[6] ?e86)))
(flet ($e148 (bvugt ?e65 (sign_extend[6] ?e24)))
(flet ($e149 (bvugt (sign_extend[11] ?e85) ?e50))
(flet ($e150 (bvult (zero_extend[4] ?e91) ?e71))
(flet ($e151 (= (zero_extend[5] ?e18) ?e77))
(flet ($e152 (bvult (zero_extend[14] ?e93) ?e43))
(flet ($e153 (bvsge ?e46 (sign_extend[3] ?e70)))
(flet ($e154 (= v0 (sign_extend[8] ?e51)))
(flet ($e155 (distinct ?e78 (sign_extend[3] ?e11)))
(flet ($e156 (= ?e23 ?e25))
(flet ($e157 (bvslt (zero_extend[1] ?e60) ?e67))
(flet ($e158 (bvule ?e74 (zero_extend[13] ?e25)))
(flet ($e159 (bvsgt ?e46 ?e50))
(flet ($e160 (bvult (sign_extend[12] ?e93) ?e84))
(flet ($e161 (= ?e70 (zero_extend[9] ?e82)))
(flet ($e162 (bvugt (sign_extend[14] ?e63) ?e62))
(flet ($e163 (bvslt ?e67 (zero_extend[7] ?e14)))
(flet ($e164 (= ?e54 ?e54))
(flet ($e165 (bvslt ?e67 (sign_extend[7] ?e49)))
(flet ($e166 (bvugt ?e36 (zero_extend[12] ?e94)))
(flet ($e167 (bvsle (zero_extend[1] ?e13) ?e49))
(flet ($e168 (bvule (zero_extend[4] ?e18) ?e44))
(flet ($e169 (bvult (zero_extend[3] ?e92) ?e13))
(flet ($e170 (bvuge ?e70 (zero_extend[9] ?e20)))
(flet ($e171 (bvule (zero_extend[10] ?e56) ?e64))
(flet ($e172 (distinct (sign_extend[12] ?e80) ?e54))
(flet ($e173 (bvult (sign_extend[5] ?e88) ?e71))
(flet ($e174 (bvsge ?e50 (zero_extend[12] ?e75)))
(flet ($e175 (bvsgt ?e36 (sign_extend[12] ?e66)))
(flet ($e176 (bvslt (zero_extend[4] ?e51) ?e91))
(flet ($e177 (bvugt (zero_extend[3] ?e65) ?e86))
(flet ($e178 (= ?e60 ?e54))
(flet ($e179 (bvslt v2 ?e18))
(flet ($e180 (bvslt (zero_extend[10] ?e25) v2))
(flet ($e181 (bvule ?e91 (sign_extend[4] ?e51)))
(flet ($e182 (bvule ?e79 (zero_extend[10] ?e13)))
(flet ($e183 (bvult ?e50 (zero_extend[9] ?e17)))
(flet ($e184 (bvsgt ?e36 (sign_extend[12] ?e31)))
(flet ($e185 (bvult (sign_extend[5] ?e18) ?e64))
(flet ($e186 (bvule v2 (zero_extend[6] ?e38)))
(flet ($e187 (bvsgt ?e62 (sign_extend[14] ?e31)))
(flet ($e188 (bvsle ?e70 (zero_extend[1] ?e12)))
(flet ($e189 (bvugt ?e22 (zero_extend[10] ?e20)))
(flet ($e190 (bvsle (zero_extend[10] ?e31) ?e21))
(flet ($e191 (bvsge (sign_extend[3] ?e36) ?e90))
(flet ($e192 (bvule (zero_extend[4] ?e31) ?e38))
(flet ($e193 (bvugt ?e91 (sign_extend[8] v1)))
(flet ($e194 (bvuge (sign_extend[2] ?e11) ?e74))
(flet ($e195 (distinct (sign_extend[13] ?e16) ?e67))
(flet ($e196 (bvugt (zero_extend[6] ?e14) ?e36))
(flet ($e197 (bvsgt ?e64 (zero_extend[15] ?e63)))
(flet ($e198 (bvult ?e89 ?e89))
(flet ($e199 (bvsgt ?e19 (zero_extend[15] ?e25)))
(flet ($e200 (bvuge (zero_extend[9] ?e69) ?e86))
(flet ($e201 (bvule ?e71 (zero_extend[8] ?e49)))
(flet ($e202 (bvsgt ?e77 (zero_extend[2] ?e35)))
(flet ($e203 (distinct (sign_extend[7] ?e14) ?e68))
(flet ($e204 (distinct ?e78 ?e78))
(flet ($e205 (bvsge (zero_extend[10] ?e31) ?e22))
(flet ($e206 (bvsge ?e56 (zero_extend[5] ?e75)))
(flet ($e207 (bvult ?e20 ?e82))
(flet ($e208 (bvsge ?e79 (zero_extend[10] ?e56)))
(flet ($e209 (= (zero_extend[5] ?e12) ?e74))
(flet ($e210 (bvult (sign_extend[14] ?e93) ?e37))
(flet ($e211 (bvugt (zero_extend[11] ?e52) ?e11))
(flet ($e212 (bvugt (zero_extend[10] ?e66) ?e91))
(flet ($e213 (bvugt (zero_extend[14] ?e52) ?e44))
(flet ($e214 (bvuge ?e35 (zero_extend[13] ?e52)))
(flet ($e215 (bvsge (zero_extend[9] ?e34) ?e68))
(flet ($e216 (distinct ?e51 ?e51))
(flet ($e217 (bvule ?e37 (sign_extend[12] v1)))
(flet ($e218 (bvsle ?e18 (sign_extend[10] ?e31)))
(flet ($e219 (bvuge (zero_extend[9] ?e16) ?e86))
(flet ($e220 (distinct ?e15 ?e79))
(flet ($e221 (= a3 a3))
(flet ($e222 (xor $e106 $e207))
(flet ($e223 (xor $e143 $e193))
(flet ($e224 (xor $e218 $e144))
(flet ($e225 (or $e161 $e165))
(flet ($e226 (if_then_else $e194 $e136 $e108))
(flet ($e227 (and $e168 $e183))
(flet ($e228 (xor $e221 $e125))
(flet ($e229 (not $e154))
(flet ($e230 (or $e114 $e173))
(flet ($e231 (iff $e105 $e132))
(flet ($e232 (xor $e130 $e181))
(flet ($e233 (xor $e199 $e96))
(flet ($e234 (implies $e148 $e150))
(flet ($e235 (xor $e200 $e210))
(flet ($e236 (iff $e158 $e220))
(flet ($e237 (or $e184 $e107))
(flet ($e238 (xor $e223 $e120))
(flet ($e239 (not $e115))
(flet ($e240 (not $e172))
(flet ($e241 (iff $e118 $e126))
(flet ($e242 (not $e198))
(flet ($e243 (if_then_else $e236 $e98 $e188))
(flet ($e244 (xor $e170 $e127))
(flet ($e245 (not $e190))
(flet ($e246 (iff $e95 $e102))
(flet ($e247 (and $e121 $e149))
(flet ($e248 (implies $e109 $e197))
(flet ($e249 (and $e164 $e216))
(flet ($e250 (not $e234))
(flet ($e251 (and $e152 $e233))
(flet ($e252 (or $e238 $e176))
(flet ($e253 (and $e116 $e187))
(flet ($e254 (implies $e145 $e249))
(flet ($e255 (implies $e229 $e206))
(flet ($e256 (xor $e101 $e112))
(flet ($e257 (xor $e97 $e178))
(flet ($e258 (or $e119 $e124))
(flet ($e259 (if_then_else $e133 $e141 $e215))
(flet ($e260 (xor $e196 $e248))
(flet ($e261 (or $e237 $e251))
(flet ($e262 (and $e205 $e201))
(flet ($e263 (xor $e192 $e128))
(flet ($e264 (if_then_else $e103 $e254 $e163))
(flet ($e265 (if_then_else $e182 $e250 $e224))
(flet ($e266 (implies $e203 $e204))
(flet ($e267 (implies $e252 $e253))
(flet ($e268 (iff $e167 $e159))
(flet ($e269 (implies $e232 $e137))
(flet ($e270 (or $e169 $e259))
(flet ($e271 (not $e142))
(flet ($e272 (or $e255 $e202))
(flet ($e273 (implies $e217 $e104))
(flet ($e274 (or $e231 $e257))
(flet ($e275 (xor $e214 $e227))
(flet ($e276 (if_then_else $e162 $e195 $e122))
(flet ($e277 (xor $e230 $e153))
(flet ($e278 (or $e242 $e186))
(flet ($e279 (and $e185 $e222))
(flet ($e280 (and $e177 $e262))
(flet ($e281 (if_then_else $e260 $e189 $e267))
(flet ($e282 (and $e160 $e270))
(flet ($e283 (not $e129))
(flet ($e284 (xor $e264 $e146))
(flet ($e285 (implies $e147 $e284))
(flet ($e286 (if_then_else $e247 $e123 $e274))
(flet ($e287 (xor $e265 $e175))
(flet ($e288 (not $e174))
(flet ($e289 (iff $e244 $e157))
(flet ($e290 (implies $e281 $e281))
(flet ($e291 (and $e289 $e110))
(flet ($e292 (iff $e211 $e179))
(flet ($e293 (implies $e279 $e191))
(flet ($e294 (implies $e272 $e266))
(flet ($e295 (iff $e140 $e166))
(flet ($e296 (implies $e287 $e100))
(flet ($e297 (not $e213))
(flet ($e298 (and $e286 $e171))
(flet ($e299 (if_then_else $e246 $e228 $e292))
(flet ($e300 (and $e256 $e297))
(flet ($e301 (not $e240))
(flet ($e302 (and $e282 $e245))
(flet ($e303 (xor $e280 $e298))
(flet ($e304 (not $e235))
(flet ($e305 (not $e225))
(flet ($e306 (or $e300 $e277))
(flet ($e307 (implies $e268 $e209))
(flet ($e308 (not $e263))
(flet ($e309 (iff $e117 $e285))
(flet ($e310 (not $e156))
(flet ($e311 (implies $e151 $e288))
(flet ($e312 (or $e275 $e306))
(flet ($e313 (iff $e271 $e243))
(flet ($e314 (if_then_else $e312 $e219 $e311))
(flet ($e315 (or $e226 $e305))
(flet ($e316 (implies $e290 $e241))
(flet ($e317 (or $e139 $e309))
(flet ($e318 (xor $e299 $e301))
(flet ($e319 (iff $e314 $e310))
(flet ($e320 (and $e295 $e135))
(flet ($e321 (not $e269))
(flet ($e322 (if_then_else $e278 $e321 $e278))
(flet ($e323 (if_then_else $e131 $e155 $e276))
(flet ($e324 (and $e261 $e212))
(flet ($e325 (iff $e307 $e323))
(flet ($e326 (implies $e316 $e113))
(flet ($e327 (not $e291))
(flet ($e328 (xor $e99 $e313))
(flet ($e329 (and $e308 $e304))
(flet ($e330 (implies $e322 $e318))
(flet ($e331 (xor $e138 $e319))
(flet ($e332 (and $e180 $e315))
(flet ($e333 (iff $e283 $e283))
(flet ($e334 (implies $e332 $e325))
(flet ($e335 (xor $e324 $e327))
(flet ($e336 (xor $e317 $e303))
(flet ($e337 (xor $e296 $e302))
(flet ($e338 (iff $e335 $e337))
(flet ($e339 (iff $e326 $e326))
(flet ($e340 (and $e339 $e111))
(flet ($e341 (or $e328 $e330))
(flet ($e342 (not $e340))
(flet ($e343 (if_then_else $e320 $e320 $e333))
(flet ($e344 (iff $e336 $e329))
(flet ($e345 (if_then_else $e334 $e331 $e294))
(flet ($e346 (not $e345))
(flet ($e347 (xor $e293 $e293))
(flet ($e348 (and $e347 $e239))
(flet ($e349 (iff $e208 $e341))
(flet ($e350 (implies $e338 $e343))
(flet ($e351 (iff $e258 $e342))
(flet ($e352 (implies $e134 $e134))
(flet ($e353 (if_then_else $e350 $e344 $e351))
(flet ($e354 (if_then_else $e353 $e346 $e273))
(flet ($e355 (and $e348 $e354))
(flet ($e356 (iff $e352 $e349))
(flet ($e357 (xor $e355 $e356))
$e357
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))