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