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