(benchmark fuzzsmt
:logic QF_AUFLIA
:status sat
:extrafuns ((f0 Int Int))
:extrafuns ((f1 Array Array))
:extrapreds ((p0 Int Int Int))
:extrapreds ((p1 Array Array Array))
:extrafuns ((v0 Int))
:extrafuns ((v1 Int))
:extrafuns ((v2 Array))
:extrafuns ((v3 Array))
:formula
(let (?e4 1)
(let (?e5 (+ v0 v0))
(let (?e6 (f0 v0))
(let (?e7 (ite (p0 ?e6 v1 ?e5) 1 0))
(let (?e8 (* v0 ?e4))
(let (?e9 (select v3 ?e6))
(let (?e10 (select v3 ?e5))
(let (?e11 (f1 v3))
(let (?e12 (f1 ?e11))
(let (?e13 (f1 ?e12))
(let (?e14 (f1 v2))
(flet ($e15 (p1 v3 v3 v3))
(flet ($e16 (p1 ?e11 ?e11 ?e13))
(flet ($e17 (p1 ?e14 ?e13 ?e12))
(flet ($e18 (p1 v2 v3 ?e11))
(flet ($e19 (p0 v1 ?e9 v0))
(flet ($e20 (p0 ?e8 v1 ?e7))
(flet ($e21 (> v0 ?e6))
(flet ($e22 (< ?e5 ?e10))
(let (?e23 (ite $e20 ?e12 ?e12))
(let (?e24 (ite $e21 ?e23 v3))
(let (?e25 (ite $e22 ?e13 ?e12))
(let (?e26 (ite $e18 v2 ?e24))
(let (?e27 (ite $e15 ?e11 ?e26))
(let (?e28 (ite $e22 ?e14 ?e26))
(let (?e29 (ite $e16 ?e13 ?e23))
(let (?e30 (ite $e17 ?e11 ?e28))
(let (?e31 (ite $e19 ?e13 ?e11))
(let (?e32 (ite $e21 v0 ?e7))
(let (?e33 (ite $e20 ?e8 v1))
(let (?e34 (ite $e20 ?e32 ?e32))
(let (?e35 (ite $e16 v1 ?e8))
(let (?e36 (ite $e17 ?e6 ?e7))
(let (?e37 (ite $e19 ?e32 ?e7))
(let (?e38 (ite $e21 ?e9 ?e8))
(let (?e39 (ite $e15 ?e10 ?e37))
(let (?e40 (ite $e19 ?e7 ?e6))
(let (?e41 (ite $e22 ?e5 ?e8))
(let (?e42 (ite $e18 ?e32 ?e8))
(let (?e43 (select ?e13 ?e35))
(let (?e44 (select ?e26 ?e37))
(let (?e45 (f1 ?e26))
(let (?e46 (f1 ?e12))
(let (?e47 (f1 ?e25))
(let (?e48 (f1 ?e25))
(let (?e49 (f1 ?e24))
(let (?e50 (f1 ?e14))
(let (?e51 (f1 ?e23))
(let (?e52 (f1 ?e27))
(let (?e53 (f1 ?e30))
(let (?e54 (f1 ?e29))
(let (?e55 (f1 ?e31))
(let (?e56 (f1 v3))
(let (?e57 (f1 ?e50))
(let (?e58 (f1 ?e13))
(let (?e59 (f1 ?e11))
(let (?e60 (f1 ?e12))
(let (?e61 (f1 ?e28))
(let (?e62 (f1 ?e49))
(let (?e63 (f1 v2))
(let (?e64 (f0 ?e36))
(let (?e65 (+ v0 ?e36))
(let (?e66 (- v1 ?e35))
(let (?e67 (f0 ?e65))
(let (?e68 (f0 ?e32))
(let (?e69 (f0 ?e6))
(let (?e70 (- ?e35 ?e68))
(let (?e71 (* ?e4 ?e40))
(let (?e72 (~ ?e42))
(let (?e73 (- ?e38 ?e37))
(let (?e74 (~ ?e39))
(let (?e75 (ite (p0 ?e64 ?e34 ?e70) 1 0))
(let (?e76 (- ?e10 ?e5))
(let (?e77 (* ?e41 ?e4))
(let (?e78 (ite (p0 ?e73 ?e7 ?e34) 1 0))
(let (?e79 (~ ?e10))
(let (?e80 (- ?e42 ?e64))
(let (?e81 (* ?e10 (~ ?e4)))
(let (?e82 (+ ?e9 ?e69))
(let (?e83 (- ?e34 ?e39))
(let (?e84 (~ ?e33))
(let (?e85 (+ ?e43 ?e33))
(let (?e86 (- ?e37 ?e37))
(let (?e87 (ite (p0 ?e5 ?e64 ?e83) 1 0))
(let (?e88 (f0 ?e74))
(let (?e89 (ite (p0 ?e88 ?e9 ?e73) 1 0))
(let (?e90 (+ ?e88 ?e80))
(let (?e91 (- ?e8 ?e8))
(let (?e92 (~ ?e44))
(flet ($e93 (p1 ?e52 ?e59 ?e30))
(flet ($e94 (p1 ?e61 ?e29 ?e46))
(flet ($e95 (p1 ?e51 ?e50 ?e63))
(flet ($e96 (p1 ?e13 ?e63 ?e23))
(flet ($e97 (p1 ?e57 ?e25 ?e57))
(flet ($e98 (p1 v2 ?e58 ?e31))
(flet ($e99 (p1 ?e14 ?e28 ?e14))
(flet ($e100 (p1 ?e62 ?e57 ?e30))
(flet ($e101 (p1 ?e53 ?e12 ?e62))
(flet ($e102 (p1 ?e49 ?e12 ?e52))
(flet ($e103 (p1 ?e46 ?e49 ?e14))
(flet ($e104 (p1 ?e57 v2 ?e31))
(flet ($e105 (p1 ?e24 ?e55 ?e14))
(flet ($e106 (p1 ?e53 ?e59 ?e30))
(flet ($e107 (p1 v3 ?e11 ?e30))
(flet ($e108 (p1 ?e56 ?e59 ?e60))
(flet ($e109 (p1 ?e62 ?e23 ?e55))
(flet ($e110 (p1 ?e29 ?e59 ?e51))
(flet ($e111 (p1 ?e30 ?e28 ?e59))
(flet ($e112 (p1 v2 ?e54 ?e13))
(flet ($e113 (p1 ?e14 ?e50 ?e48))
(flet ($e114 (p1 ?e26 ?e60 ?e30))
(flet ($e115 (p1 ?e27 ?e12 ?e47))
(flet ($e116 (p1 ?e45 ?e53 ?e62))
(flet ($e117 (<= ?e91 ?e85))
(flet ($e118 (>= ?e40 ?e89))
(flet ($e119 (distinct ?e76 ?e77))
(flet ($e120 (>= ?e91 ?e5))
(flet ($e121 (= ?e84 ?e68))
(flet ($e122 (p0 ?e41 v1 ?e36))
(flet ($e123 (= ?e77 ?e69))
(flet ($e124 (> ?e38 ?e10))
(flet ($e125 (p0 v1 ?e77 ?e5))
(flet ($e126 (= ?e64 ?e41))
(flet ($e127 (>= ?e81 ?e40))
(flet ($e128 (< ?e67 ?e39))
(flet ($e129 (distinct ?e78 ?e65))
(flet ($e130 (<= ?e34 ?e33))
(flet ($e131 (<= ?e72 ?e76))
(flet ($e132 (> ?e87 ?e88))
(flet ($e133 (>= ?e92 ?e8))
(flet ($e134 (>= ?e86 ?e36))
(flet ($e135 (> ?e32 ?e33))
(flet ($e136 (distinct ?e90 ?e6))
(flet ($e137 (< ?e88 ?e35))
(flet ($e138 (p0 ?e9 ?e38 ?e78))
(flet ($e139 (> ?e80 ?e32))
(flet ($e140 (p0 ?e79 ?e91 ?e88))
(flet ($e141 (p0 ?e75 ?e10 ?e74))
(flet ($e142 (>= ?e34 ?e39))
(flet ($e143 (p0 ?e66 ?e67 ?e66))
(flet ($e144 (= ?e90 ?e39))
(flet ($e145 (< ?e37 ?e79))
(flet ($e146 (distinct ?e44 ?e78))
(flet ($e147 (< ?e83 v0))
(flet ($e148 (>= ?e7 ?e69))
(flet ($e149 (>= ?e73 ?e10))
(flet ($e150 (p0 ?e71 ?e90 ?e65))
(flet ($e151 (p0 ?e36 ?e33 ?e33))
(flet ($e152 (> ?e82 ?e80))
(flet ($e153 (distinct ?e79 ?e10))
(flet ($e154 (p0 ?e42 ?e64 v0))
(flet ($e155 (< ?e70 ?e86))
(flet ($e156 (<= ?e43 ?e7))
(flet ($e157 (or $e16 $e139))
(flet ($e158 (if_then_else $e103 $e93 $e141))
(flet ($e159 (not $e132))
(flet ($e160 (or $e111 $e100))
(flet ($e161 (iff $e160 $e134))
(flet ($e162 (and $e19 $e133))
(flet ($e163 (and $e146 $e128))
(flet ($e164 (and $e157 $e156))
(flet ($e165 (xor $e140 $e155))
(flet ($e166 (implies $e113 $e153))
(flet ($e167 (iff $e164 $e102))
(flet ($e168 (implies $e121 $e116))
(flet ($e169 (if_then_else $e142 $e119 $e104))
(flet ($e170 (implies $e129 $e99))
(flet ($e171 (or $e135 $e161))
(flet ($e172 (or $e126 $e15))
(flet ($e173 (implies $e158 $e137))
(flet ($e174 (iff $e166 $e117))
(flet ($e175 (iff $e105 $e174))
(flet ($e176 (not $e125))
(flet ($e177 (iff $e120 $e171))
(flet ($e178 (xor $e168 $e149))
(flet ($e179 (and $e96 $e96))
(flet ($e180 (and $e130 $e143))
(flet ($e181 (and $e108 $e20))
(flet ($e182 (if_then_else $e173 $e159 $e167))
(flet ($e183 (xor $e118 $e107))
(flet ($e184 (implies $e98 $e169))
(flet ($e185 (and $e177 $e136))
(flet ($e186 (not $e185))
(flet ($e187 (and $e170 $e138))
(flet ($e188 (iff $e109 $e147))
(flet ($e189 (or $e188 $e145))
(flet ($e190 (implies $e152 $e94))
(flet ($e191 (if_then_else $e97 $e181 $e163))
(flet ($e192 (iff $e115 $e190))
(flet ($e193 (if_then_else $e183 $e172 $e17))
(flet ($e194 (not $e127))
(flet ($e195 (iff $e179 $e101))
(flet ($e196 (iff $e186 $e154))
(flet ($e197 (if_then_else $e178 $e176 $e150))
(flet ($e198 (xor $e122 $e124))
(flet ($e199 (not $e182))
(flet ($e200 (and $e112 $e197))
(flet ($e201 (iff $e151 $e184))
(flet ($e202 (or $e106 $e192))
(flet ($e203 (iff $e162 $e95))
(flet ($e204 (and $e199 $e199))
(flet ($e205 (if_then_else $e131 $e187 $e131))
(flet ($e206 (xor $e144 $e201))
(flet ($e207 (and $e18 $e202))
(flet ($e208 (and $e193 $e22))
(flet ($e209 (or $e123 $e203))
(flet ($e210 (not $e196))
(flet ($e211 (and $e209 $e200))
(flet ($e212 (xor $e208 $e114))
(flet ($e213 (xor $e212 $e175))
(flet ($e214 (and $e148 $e206))
(flet ($e215 (or $e198 $e210))
(flet ($e216 (or $e213 $e215))
(flet ($e217 (xor $e189 $e194))
(flet ($e218 (and $e214 $e204))
(flet ($e219 (and $e211 $e21))
(flet ($e220 (and $e165 $e191))
(flet ($e221 (xor $e180 $e180))
(flet ($e222 (and $e218 $e205))
(flet ($e223 (iff $e195 $e219))
(flet ($e224 (not $e221))
(flet ($e225 (iff $e222 $e220))
(flet ($e226 (implies $e225 $e223))
(flet ($e227 (not $e207))
(flet ($e228 (if_then_else $e226 $e226 $e216))
(flet ($e229 (iff $e217 $e110))
(flet ($e230 (not $e229))
(flet ($e231 (if_then_else $e224 $e230 $e227))
(flet ($e232 (or $e231 $e228))
$e232
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))