(benchmark fuzzsmt
:logic QF_AUFLIA
:status sat
:extrafuns ((f0 Int Int))
:extrafuns ((f1 Array Array Array))
:extrapreds ((p0 Int))
:extrapreds ((p1 Array Array Array))
:extrafuns ((v0 Int))
:extrafuns ((v1 Array))
:formula
(let (?e2 0)
(let (?e3 (ite (p0 v0) 1 0))
(let (?e4 (ite (p0 v0) 1 0))
(let (?e5 (~ ?e4))
(let (?e6 (ite (p0 ?e3) 1 0))
(let (?e7 (f0 ?e3))
(let (?e8 (* ?e4 (~ ?e2)))
(let (?e9 (store v1 ?e5 ?e8))
(let (?e10 (select ?e9 ?e4))
(let (?e11 (store ?e9 ?e8 ?e7))
(let (?e12 (select ?e11 ?e10))
(let (?e13 (f1 ?e11 ?e11))
(let (?e14 (f1 v1 ?e13))
(let (?e15 (f1 ?e9 ?e13))
(flet ($e16 (p1 ?e14 ?e11 ?e15))
(flet ($e17 (p1 ?e13 ?e15 v1))
(flet ($e18 (p1 ?e9 ?e9 ?e14))
(flet ($e19 (p0 ?e7))
(flet ($e20 (<= v0 ?e4))
(flet ($e21 (> ?e7 ?e12))
(flet ($e22 (= ?e7 ?e12))
(flet ($e23 (distinct ?e6 ?e5))
(flet ($e24 (p0 ?e7))
(flet ($e25 (>= ?e3 ?e8))
(flet ($e26 (< ?e3 ?e7))
(flet ($e27 (<= ?e7 v0))
(flet ($e28 (p0 ?e10))
(let (?e29 (ite $e27 ?e15 ?e13))
(let (?e30 (ite $e28 ?e14 ?e14))
(let (?e31 (ite $e26 ?e9 v1))
(let (?e32 (ite $e17 ?e11 ?e13))
(let (?e33 (ite $e23 ?e13 ?e13))
(let (?e34 (ite $e25 ?e14 ?e30))
(let (?e35 (ite $e22 ?e30 ?e30))
(let (?e36 (ite $e25 ?e11 ?e31))
(let (?e37 (ite $e22 ?e14 ?e35))
(let (?e38 (ite $e19 ?e36 ?e35))
(let (?e39 (ite $e21 ?e36 ?e9))
(let (?e40 (ite $e16 ?e39 ?e11))
(let (?e41 (ite $e28 ?e29 v1))
(let (?e42 (ite $e25 ?e33 ?e36))
(let (?e43 (ite $e21 ?e29 ?e9))
(let (?e44 (ite $e18 ?e30 ?e13))
(let (?e45 (ite $e18 ?e11 ?e41))
(let (?e46 (ite $e20 ?e15 ?e34))
(let (?e47 (ite $e24 ?e40 ?e13))
(let (?e48 (ite $e26 ?e7 ?e6))
(let (?e49 (ite $e21 ?e10 ?e6))
(let (?e50 (ite $e22 v0 ?e8))
(let (?e51 (ite $e19 ?e5 ?e4))
(let (?e52 (ite $e16 ?e12 ?e10))
(let (?e53 (ite $e16 ?e49 ?e8))
(let (?e54 (ite $e21 ?e3 v0))
(let (?e55 (ite $e24 ?e51 ?e52))
(let (?e56 (ite $e23 ?e10 ?e5))
(let (?e57 (ite $e18 ?e50 ?e49))
(let (?e58 (ite $e17 ?e10 ?e4))
(let (?e59 (ite $e27 ?e57 ?e12))
(let (?e60 (ite $e21 ?e10 ?e3))
(let (?e61 (ite $e28 ?e7 ?e55))
(let (?e62 (ite $e20 ?e53 ?e53))
(let (?e63 (ite $e25 ?e48 ?e8))
(let (?e64 (store ?e45 ?e49 ?e8))
(let (?e65 (store ?e43 ?e55 ?e57))
(let (?e66 (select ?e34 v0))
(let (?e67 (store ?e9 ?e66 ?e54))
(let (?e68 (select ?e64 ?e56))
(let (?e69 (f1 ?e11 ?e30))
(let (?e70 (f1 ?e34 ?e36))
(let (?e71 (f1 ?e38 ?e39))
(let (?e72 (f1 ?e31 ?e45))
(let (?e73 (f1 ?e43 ?e43))
(let (?e74 (f1 ?e37 ?e65))
(let (?e75 (f1 ?e9 ?e38))
(let (?e76 (f1 ?e37 ?e14))
(let (?e77 (f1 ?e13 ?e39))
(let (?e78 (f1 ?e34 ?e39))
(let (?e79 (f1 ?e64 ?e64))
(let (?e80 (f1 ?e15 ?e15))
(let (?e81 (f1 v1 v1))
(let (?e82 (f1 ?e47 ?e71))
(let (?e83 (f1 ?e77 ?e13))
(let (?e84 (f1 ?e32 ?e32))
(let (?e85 (f1 ?e46 ?e46))
(let (?e86 (f1 ?e36 ?e72))
(let (?e87 (f1 ?e81 ?e65))
(let (?e88 (f1 ?e29 ?e45))
(let (?e89 (f1 ?e44 ?e31))
(let (?e90 (f1 ?e41 ?e41))
(let (?e91 (f1 ?e34 ?e42))
(let (?e92 (f1 ?e35 ?e35))
(let (?e93 (f1 ?e33 ?e33))
(let (?e94 (f1 ?e11 ?e14))
(let (?e95 (f1 ?e67 ?e34))
(let (?e96 (f1 ?e86 ?e37))
(let (?e97 (f1 ?e40 ?e40))
(let (?e98 (- ?e56 ?e5))
(let (?e99 (+ ?e52 ?e57))
(let (?e100 (ite (p0 ?e51) 1 0))
(let (?e101 (ite (p0 ?e12) 1 0))
(let (?e102 (ite (p0 ?e58) 1 0))
(let (?e103 (+ v0 ?e10))
(let (?e104 (~ ?e48))
(let (?e105 (* ?e2 ?e12))
(let (?e106 (- ?e3 ?e101))
(let (?e107 (- ?e59 ?e100))
(let (?e108 (ite (p0 ?e10) 1 0))
(let (?e109 (* ?e2 ?e102))
(let (?e110 (ite (p0 ?e7) 1 0))
(let (?e111 (* ?e53 (~ ?e2)))
(let (?e112 (* ?e2 ?e4))
(let (?e113 (~ ?e106))
(let (?e114 (~ ?e57))
(let (?e115 (* ?e68 (~ ?e2)))
(let (?e116 (- ?e4 ?e50))
(let (?e117 (* ?e2 ?e49))
(let (?e118 (ite (p0 ?e61) 1 0))
(let (?e119 (ite (p0 ?e62) 1 0))
(let (?e120 (* ?e10 ?e2))
(let (?e121 (ite (p0 ?e119) 1 0))
(let (?e122 (f0 ?e55))
(let (?e123 (* (~ ?e2) ?e66))
(let (?e124 (* ?e2 ?e63))
(let (?e125 (ite (p0 ?e106) 1 0))
(let (?e126 (f0 ?e102))
(let (?e127 (f0 ?e55))
(let (?e128 (f0 ?e103))
(let (?e129 (~ ?e8))
(let (?e130 (- ?e126 ?e6))
(let (?e131 (* (~ ?e2) ?e60))
(let (?e132 (* (~ ?e2) ?e54))
(flet ($e133 (p1 ?e15 ?e73 ?e14))
(flet ($e134 (p1 ?e47 ?e78 ?e81))
(flet ($e135 (p1 ?e44 ?e80 ?e37))
(flet ($e136 (p1 ?e42 ?e73 ?e91))
(flet ($e137 (p1 ?e43 ?e37 ?e14))
(flet ($e138 (p1 ?e73 ?e87 ?e34))
(flet ($e139 (p1 ?e75 ?e46 ?e75))
(flet ($e140 (p1 ?e96 ?e96 ?e88))
(flet ($e141 (p1 ?e89 ?e78 ?e87))
(flet ($e142 (p1 ?e70 ?e95 ?e47))
(flet ($e143 (p1 ?e39 ?e96 ?e74))
(flet ($e144 (p1 ?e91 ?e72 ?e70))
(flet ($e145 (p1 v1 ?e65 ?e44))
(flet ($e146 (p1 ?e90 ?e70 ?e79))
(flet ($e147 (p1 ?e94 ?e91 ?e13))
(flet ($e148 (p1 ?e41 ?e93 ?e32))
(flet ($e149 (p1 ?e40 ?e91 ?e93))
(flet ($e150 (p1 ?e92 ?e34 ?e80))
(flet ($e151 (p1 ?e71 ?e44 ?e78))
(flet ($e152 (p1 ?e43 ?e34 ?e73))
(flet ($e153 (p1 ?e81 ?e73 ?e70))
(flet ($e154 (p1 ?e86 ?e86 ?e38))
(flet ($e155 (p1 ?e45 v1 ?e36))
(flet ($e156 (p1 ?e43 ?e30 ?e37))
(flet ($e157 (p1 ?e84 ?e78 ?e45))
(flet ($e158 (p1 ?e67 ?e38 ?e90))
(flet ($e159 (p1 ?e31 ?e81 ?e13))
(flet ($e160 (p1 ?e64 ?e47 ?e94))
(flet ($e161 (p1 ?e29 ?e75 ?e76))
(flet ($e162 (p1 ?e85 ?e96 ?e82))
(flet ($e163 (p1 ?e33 ?e29 ?e38))
(flet ($e164 (p1 ?e31 ?e78 ?e69))
(flet ($e165 (p1 ?e97 ?e9 ?e35))
(flet ($e166 (p1 ?e83 ?e71 ?e79))
(flet ($e167 (p1 ?e11 ?e67 ?e31))
(flet ($e168 (p1 ?e39 ?e93 ?e96))
(flet ($e169 (p1 ?e65 ?e85 ?e44))
(flet ($e170 (p1 ?e76 ?e40 ?e15))
(flet ($e171 (p1 ?e77 ?e34 ?e14))
(flet ($e172 (distinct ?e129 ?e62))
(flet ($e173 (p0 ?e116))
(flet ($e174 (> ?e120 ?e10))
(flet ($e175 (p0 ?e102))
(flet ($e176 (> ?e50 ?e53))
(flet ($e177 (> ?e119 ?e127))
(flet ($e178 (distinct ?e117 ?e55))
(flet ($e179 (= ?e122 ?e102))
(flet ($e180 (< ?e123 ?e52))
(flet ($e181 (> ?e66 ?e51))
(flet ($e182 (= ?e121 ?e4))
(flet ($e183 (distinct ?e130 ?e102))
(flet ($e184 (< ?e111 ?e4))
(flet ($e185 (p0 ?e68))
(flet ($e186 (distinct ?e3 ?e3))
(flet ($e187 (>= ?e66 ?e59))
(flet ($e188 (< ?e10 ?e48))
(flet ($e189 (distinct ?e5 ?e52))
(flet ($e190 (= ?e101 ?e54))
(flet ($e191 (>= ?e8 ?e116))
(flet ($e192 (<= ?e62 ?e12))
(flet ($e193 (< ?e131 ?e114))
(flet ($e194 (>= ?e49 ?e125))
(flet ($e195 (> ?e100 ?e7))
(flet ($e196 (p0 ?e101))
(flet ($e197 (distinct ?e118 ?e52))
(flet ($e198 (<= v0 ?e60))
(flet ($e199 (p0 ?e128))
(flet ($e200 (>= ?e6 ?e106))
(flet ($e201 (= ?e50 ?e61))
(flet ($e202 (> ?e115 ?e132))
(flet ($e203 (distinct ?e57 ?e102))
(flet ($e204 (>= ?e102 ?e55))
(flet ($e205 (p0 ?e55))
(flet ($e206 (<= ?e113 ?e132))
(flet ($e207 (<= ?e124 ?e106))
(flet ($e208 (> ?e68 ?e117))
(flet ($e209 (p0 ?e56))
(flet ($e210 (<= ?e63 ?e112))
(flet ($e211 (<= ?e119 ?e5))
(flet ($e212 (= ?e105 ?e51))
(flet ($e213 (< ?e6 ?e118))
(flet ($e214 (p0 ?e66))
(flet ($e215 (>= ?e58 ?e101))
(flet ($e216 (distinct ?e109 ?e57))
(flet ($e217 (distinct ?e99 ?e103))
(flet ($e218 (<= ?e126 ?e58))
(flet ($e219 (>= ?e107 ?e120))
(flet ($e220 (< ?e125 ?e124))
(flet ($e221 (> ?e98 ?e105))
(flet ($e222 (p0 ?e118))
(flet ($e223 (= ?e108 ?e4))
(flet ($e224 (= ?e58 ?e114))
(flet ($e225 (< ?e110 ?e123))
(flet ($e226 (distinct ?e104 ?e111))
(flet ($e227 (iff $e179 $e21))
(flet ($e228 (if_then_else $e185 $e171 $e141))
(flet ($e229 (and $e152 $e216))
(flet ($e230 (and $e133 $e165))
(flet ($e231 (and $e155 $e217))
(flet ($e232 (iff $e16 $e180))
(flet ($e233 (if_then_else $e168 $e191 $e153))
(flet ($e234 (implies $e159 $e147))
(flet ($e235 (not $e203))
(flet ($e236 (xor $e28 $e223))
(flet ($e237 (and $e174 $e172))
(flet ($e238 (or $e194 $e197))
(flet ($e239 (iff $e149 $e201))
(flet ($e240 (not $e181))
(flet ($e241 (or $e238 $e157))
(flet ($e242 (and $e190 $e225))
(flet ($e243 (implies $e140 $e215))
(flet ($e244 (xor $e176 $e20))
(flet ($e245 (not $e241))
(flet ($e246 (iff $e243 $e158))
(flet ($e247 (iff $e18 $e169))
(flet ($e248 (xor $e173 $e210))
(flet ($e249 (if_then_else $e212 $e143 $e218))
(flet ($e250 (not $e177))
(flet ($e251 (or $e207 $e163))
(flet ($e252 (implies $e214 $e156))
(flet ($e253 (or $e170 $e166))
(flet ($e254 (iff $e206 $e209))
(flet ($e255 (and $e231 $e189))
(flet ($e256 (or $e148 $e167))
(flet ($e257 (if_then_else $e237 $e248 $e235))
(flet ($e258 (or $e138 $e142))
(flet ($e259 (or $e249 $e164))
(flet ($e260 (and $e208 $e204))
(flet ($e261 (xor $e260 $e202))
(flet ($e262 (xor $e193 $e136))
(flet ($e263 (if_then_else $e184 $e219 $e227))
(flet ($e264 (not $e145))
(flet ($e265 (or $e256 $e187))
(flet ($e266 (implies $e160 $e205))
(flet ($e267 (iff $e178 $e134))
(flet ($e268 (or $e220 $e27))
(flet ($e269 (and $e265 $e25))
(flet ($e270 (not $e242))
(flet ($e271 (or $e270 $e255))
(flet ($e272 (not $e199))
(flet ($e273 (xor $e239 $e154))
(flet ($e274 (or $e144 $e144))
(flet ($e275 (if_then_else $e267 $e230 $e258))
(flet ($e276 (not $e22))
(flet ($e277 (and $e17 $e192))
(flet ($e278 (and $e246 $e135))
(flet ($e279 (and $e228 $e234))
(flet ($e280 (and $e232 $e263))
(flet ($e281 (and $e268 $e269))
(flet ($e282 (if_then_else $e188 $e229 $e183))
(flet ($e283 (if_then_else $e150 $e276 $e236))
(flet ($e284 (if_then_else $e252 $e24 $e211))
(flet ($e285 (iff $e264 $e151))
(flet ($e286 (xor $e200 $e175))
(flet ($e287 (or $e281 $e250))
(flet ($e288 (if_then_else $e262 $e262 $e280))
(flet ($e289 (not $e26))
(flet ($e290 (if_then_else $e245 $e259 $e245))
(flet ($e291 (not $e162))
(flet ($e292 (if_then_else $e266 $e251 $e289))
(flet ($e293 (implies $e254 $e275))
(flet ($e294 (or $e273 $e293))
(flet ($e295 (xor $e272 $e224))
(flet ($e296 (implies $e257 $e240))
(flet ($e297 (iff $e253 $e23))
(flet ($e298 (iff $e19 $e292))
(flet ($e299 (implies $e282 $e196))
(flet ($e300 (iff $e284 $e139))
(flet ($e301 (implies $e297 $e283))
(flet ($e302 (and $e291 $e221))
(flet ($e303 (not $e247))
(flet ($e304 (xor $e294 $e161))
(flet ($e305 (not $e244))
(flet ($e306 (iff $e290 $e279))
(flet ($e307 (and $e300 $e182))
(flet ($e308 (implies $e288 $e195))
(flet ($e309 (if_then_else $e304 $e299 $e186))
(flet ($e310 (if_then_else $e261 $e222 $e213))
(flet ($e311 (or $e286 $e301))
(flet ($e312 (and $e311 $e298))
(flet ($e313 (and $e295 $e302))
(flet ($e314 (if_then_else $e305 $e278 $e278))
(flet ($e315 (not $e226))
(flet ($e316 (not $e303))
(flet ($e317 (not $e315))
(flet ($e318 (and $e296 $e137))
(flet ($e319 (if_then_else $e307 $e308 $e313))
(flet ($e320 (xor $e233 $e319))
(flet ($e321 (if_then_else $e317 $e310 $e274))
(flet ($e322 (not $e146))
(flet ($e323 (xor $e198 $e321))
(flet ($e324 (implies $e316 $e271))
(flet ($e325 (xor $e312 $e314))
(flet ($e326 (implies $e285 $e306))
(flet ($e327 (if_then_else $e324 $e325 $e325))
(flet ($e328 (if_then_else $e322 $e287 $e326))
(flet ($e329 (implies $e323 $e309))
(flet ($e330 (if_then_else $e327 $e329 $e318))
(flet ($e331 (if_then_else $e277 $e330 $e277))
(flet ($e332 (not $e328))
(flet ($e333 (implies $e332 $e332))
(flet ($e334 (not $e320))
(flet ($e335 (implies $e333 $e334))
(flet ($e336 (xor $e335 $e335))
(flet ($e337 (iff $e331 $e336))
$e337
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))