some failing examples

4 files changed, 820 insertions, 0 deletions

diff --git a/test/regress/regress0/aufbv/fuzz01.delta01.smt b/test/regress/regress0/aufbv/fuzz01.delta01.smt
new file mode 100644
index 000000000..93ba564a3
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz01.delta01.smt
@@ -0,0 +1,25 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((v1 BitVec[3]))
+:extrafuns ((v2 BitVec[11]))
+:extrafuns ((a9 Array[8:5]))
+:extrafuns ((a6 Array[1:13]))
+:status unknown
+:formula
+(let (?n1 bv0[15])
+(let (?n2 bv0[1])
+(let (?n3 (zero_extend[8] v1))
+(let (?n4 (bvnor v2 ?n3))
+(let (?n5 (extract[7:0] ?n4))
+(let (?n6 bv0[5])
+(let (?n7 (store a9 ?n5 ?n6))
+(let (?n8 bv0[8])
+(let (?n9 (select ?n7 ?n8))
+(let (?n10 (zero_extend[8] ?n9))
+(let (?n11 (store a6 ?n2 ?n10))
+(let (?n12 (extract[0:0] ?n4))
+(let (?n13 (select ?n11 ?n12))
+(let (?n14 (zero_extend[2] ?n13))
+(flet ($n15 (= ?n1 ?n14))
+$n15
+))))))))))))))))
diff --git a/test/regress/regress0/aufbv/fuzz01.smt b/test/regress/regress0/aufbv/fuzz01.smt
new file mode 100644
index 000000000..233427ae0
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz01.smt
@@ -0,0 +1,365 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status unknown
+: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
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/aufbv/fuzz02.delta01.smt b/test/regress/regress0/aufbv/fuzz02.delta01.smt
new file mode 100644
index 000000000..cb8833ea9
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz02.delta01.smt
@@ -0,0 +1,19 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((a5 Array[5:13]))
+:extrafuns ((v4 BitVec[11]))
+:status unknown
+:formula
+(let (?n1 bv0[11])
+(flet ($n2 (bvsle v4 ?n1))
+(let (?n3 bv1[1])
+(let (?n4 bv0[1])
+(let (?n5 (ite $n2 ?n3 ?n4))
+(let (?n6 bv0[5])
+(let (?n7 (select a5 ?n6))
+(let (?n8 bv0[13])
+(flet ($n9 (bvugt ?n7 ?n8))
+(let (?n10 (ite $n9 ?n3 ?n4))
+(flet ($n11 (bvslt ?n5 ?n10))
+$n11
+))))))))))))
diff --git a/test/regress/regress0/aufbv/fuzz02.smt b/test/regress/regress0/aufbv/fuzz02.smt
new file mode 100644
index 000000000..8b60e39fc
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz02.smt
@@ -0,0 +1,411 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status unknown
+:extrafuns ((v0 BitVec[14]))
+:extrafuns ((v1 BitVec[10]))
+:extrafuns ((v2 BitVec[10]))
+:extrafuns ((v3 BitVec[8]))
+:extrafuns ((v4 BitVec[11]))
+:extrafuns ((a5 Array[5:13]))
+:extrafuns ((a6 Array[15:15]))
+:extrafuns ((a7 Array[3:1]))
+:extrafuns ((a8 Array[8:14]))
+:extrafuns ((a9 Array[6:16]))
+:extrafuns ((a10 Array[13:9]))
+:extrafuns ((a11 Array[3:14]))
+:extrafuns ((a12 Array[1:3]))
+:formula
+(let (?e13 bv37[10])
+(let (?e14 bv27[6])
+(let (?e15 bv60[7])
+(let (?e16 bv486[9])
+(let (?e17 bv7[5])
+(let (?e18 (ite (bvsle v4 (sign_extend[6] ?e17)) bv1[1] bv0[1]))
+(let (?e19 (ite (bvsge v0 (zero_extend[4] ?e13)) bv1[1] bv0[1]))
+(let (?e20 (bvneg v3))
+(let (?e21 (rotate_left[5] v1))
+(let (?e22 (ite (bvsge v4 v4) bv1[1] bv0[1]))
+(let (?e23 (ite (= (zero_extend[4] ?e14) ?e13) bv1[1] bv0[1]))
+(let (?e24 (sign_extend[4] v2))
+(let (?e25 (bvneg ?e16))
+(let (?e26 (bvashr ?e15 (zero_extend[6] ?e23)))
+(let (?e27 (store a12 (extract[6:6] ?e21) (extract[13:11] v0)))
+(let (?e28 (store a10 (sign_extend[5] v3) (extract[9:1] v0)))
+(let (?e29 (store a12 (extract[5:5] ?e16) (extract[9:7] ?e21)))
+(let (?e30 (store a11 (extract[9:7] v0) (sign_extend[4] v1)))
+(let (?e31 (store a5 (extract[5:1] ?e14) (zero_extend[12] ?e22)))
+(let (?e32 (ite (= ?e30 ?e30) bv1[1] bv0[1]))
+(let (?e33 (select a10 (extract[13:1] v0)))
+(let (?e34 (select ?e29 (extract[2:2] ?e17)))
+(let (?e35 (select ?e30 ?e34))
+(let (?e36 (select a8 (extract[13:6] ?e35)))
+(let (?e37 (select ?e31 (extract[4:0] ?e15)))
+(let (?e38 (select a9 (extract[9:4] v1)))
+(let (?e39 (select a8 (zero_extend[1] ?e26)))
+(let (?e40 (store a7 (extract[2:0] ?e24) ?e18))
+(let (?e41 (store ?e31 (extract[11:7] ?e24) (sign_extend[12] ?e23)))
+(let (?e42 (store a8 (zero_extend[7] ?e23) ?e36))
+(let (?e43 (select ?e42 (zero_extend[1] ?e26)))
+(let (?e44 (select ?e29 (extract[6:6] v2)))
+(let (?e45 (select a5 (zero_extend[4] ?e32)))
+(let (?e46 (store a6 (sign_extend[14] ?e23) (zero_extend[1] v0)))
+(let (?e47 (select ?e27 ?e18))
+(let (?e48 (select ?e40 (extract[13:11] ?e43)))
+(let (?e49 (store a6 (zero_extend[1] ?e39) (sign_extend[14] ?e23)))
+(let (?e50 (select ?e27 (extract[10:10] ?e36)))
+(let (?e51 (bvnot ?e15))
+(let (?e52 (repeat[2] v3))
+(let (?e53 (bvmul (zero_extend[10] ?e34) ?e37))
+(let (?e54 (bvsub ?e21 (zero_extend[3] ?e15)))
+(let (?e55 (bvneg ?e39))
+(let (?e56 (bvsub (zero_extend[8] ?e17) ?e37))
+(let (?e57 (ite (bvsgt ?e24 (sign_extend[7] ?e26)) bv1[1] bv0[1]))
+(let (?e58 (bvcomp (sign_extend[9] ?e32) ?e13))
+(let (?e59 (rotate_left[3] ?e33))
+(let (?e60 (bvadd ?e37 (sign_extend[8] ?e17)))
+(let (?e61 (rotate_right[0] ?e44))
+(let (?e62 (ite (bvsgt (zero_extend[6] ?e13) ?e52) bv1[1] bv0[1]))
+(let (?e63 (ite (bvsle ?e38 (zero_extend[6] v2)) bv1[1] bv0[1]))
+(let (?e64 (ite (bvuge (zero_extend[15] ?e23) ?e52) bv1[1] bv0[1]))
+(let (?e65 (bvlshr (zero_extend[10] ?e47) ?e45))
+(let (?e66 (bvnand ?e18 ?e23))
+(let (?e67 (bvashr ?e36 (zero_extend[13] ?e58)))
+(let (?e68 (bvxnor (zero_extend[6] ?e50) ?e25))
+(let (?e69 (ite (bvugt ?e55 (sign_extend[4] v2)) bv1[1] bv0[1]))
+(let (?e70 (bvshl (zero_extend[13] ?e19) ?e35))
+(let (?e71 (bvashr (zero_extend[2] ?e23) ?e61))
+(let (?e72 (bvcomp (sign_extend[3] v2) ?e65))
+(let (?e73 (ite (bvugt ?e56 (sign_extend[7] ?e14)) bv1[1] bv0[1]))
+(let (?e74 (bvneg ?e70))
+(let (?e75 (bvsub ?e16 ?e59))
+(let (?e76 (ite (bvsgt (sign_extend[5] ?e57) ?e14) bv1[1] bv0[1]))
+(let (?e77 (repeat[3] ?e22))
+(let (?e78 (bvcomp ?e65 ?e65))
+(let (?e79 (bvneg ?e48))
+(let (?e80 (ite (bvsge (zero_extend[8] ?e20) ?e38) bv1[1] bv0[1]))
+(let (?e81 (ite (bvult (zero_extend[4] ?e68) ?e45) bv1[1] bv0[1]))
+(let (?e82 (sign_extend[1] v1))
+(let (?e83 (bvor (sign_extend[2] ?e33) v4))
+(let (?e84 (bvshl v0 ?e39))
+(let (?e85 (ite (bvugt (sign_extend[9] ?e62) v2) bv1[1] bv0[1]))
+(let (?e86 (bvnot ?e43))
+(flet ($e87 (bvsge (zero_extend[11] ?e50) ?e86))
+(flet ($e88 (bvsle ?e73 ?e76))
+(flet ($e89 (bvult ?e50 (zero_extend[2] ?e76)))
+(flet ($e90 (= ?e63 ?e79))
+(flet ($e91 (bvsgt (zero_extend[13] ?e72) ?e84))
+(flet ($e92 (bvsle (sign_extend[13] ?e44) ?e52))
+(flet ($e93 (distinct ?e32 ?e76))
+(flet ($e94 (bvult (sign_extend[8] ?e78) ?e33))
+(flet ($e95 (bvuge (sign_extend[11] ?e71) ?e35))
+(flet ($e96 (bvule (zero_extend[15] ?e72) ?e38))
+(flet ($e97 (bvsge ?e65 (zero_extend[2] ?e82)))
+(flet ($e98 (bvuge v0 (sign_extend[5] ?e33)))
+(flet ($e99 (distinct (sign_extend[2] ?e25) v4))
+(flet ($e100 (bvsge ?e33 (zero_extend[8] ?e58)))
+(flet ($e101 (bvsge ?e35 (zero_extend[11] ?e44)))
+(flet ($e102 (= ?e53 (zero_extend[12] ?e57)))
+(flet ($e103 (bvugt ?e39 (zero_extend[4] v1)))
+(flet ($e104 (bvult (zero_extend[11] ?e34) ?e24))
+(flet ($e105 (bvuge ?e47 (sign_extend[2] ?e32)))
+(flet ($e106 (bvsgt ?e84 (sign_extend[1] ?e56)))
+(flet ($e107 (bvsle ?e17 (sign_extend[4] ?e85)))
+(flet ($e108 (bvsle ?e56 (zero_extend[10] ?e61)))
+(flet ($e109 (bvsle (zero_extend[11] ?e47) ?e35))
+(flet ($e110 (bvslt ?e67 v0))
+(flet ($e111 (bvsgt (zero_extend[13] ?e69) ?e74))
+(flet ($e112 (bvslt ?e36 v0))
+(flet ($e113 (bvsge (zero_extend[3] ?e61) ?e14))
+(flet ($e114 (bvsgt (zero_extend[11] ?e61) ?e36))
+(flet ($e115 (bvsge (zero_extend[8] ?e22) ?e25))
+(flet ($e116 (bvuge ?e33 ?e59))
+(flet ($e117 (bvuge (zero_extend[5] ?e23) ?e14))
+(flet ($e118 (bvugt (sign_extend[6] ?e85) ?e51))
+(flet ($e119 (distinct (zero_extend[2] ?e69) ?e34))
+(flet ($e120 (bvugt (zero_extend[8] ?e19) ?e59))
+(flet ($e121 (distinct (zero_extend[8] ?e72) ?e75))
+(flet ($e122 (distinct v1 (zero_extend[7] ?e77)))
+(flet ($e123 (distinct ?e21 (zero_extend[3] ?e15)))
+(flet ($e124 (bvult ?e86 (zero_extend[11] ?e44)))
+(flet ($e125 (bvslt ?e60 (zero_extend[4] ?e68)))
+(flet ($e126 (distinct ?e66 ?e72))
+(flet ($e127 (bvslt v1 (sign_extend[9] ?e64)))
+(flet ($e128 (bvult (zero_extend[8] ?e23) ?e68))
+(flet ($e129 (bvult (zero_extend[1] v3) ?e33))
+(flet ($e130 (= (sign_extend[6] ?e32) ?e26))
+(flet ($e131 (bvsgt ?e84 (zero_extend[13] ?e76)))
+(flet ($e132 (bvslt ?e24 (sign_extend[6] v3)))
+(flet ($e133 (bvugt ?e33 (zero_extend[6] ?e34)))
+(flet ($e134 (bvsgt ?e68 (sign_extend[8] ?e57)))
+(flet ($e135 (bvult ?e84 (zero_extend[11] ?e44)))
+(flet ($e136 (bvsle (zero_extend[10] ?e50) ?e53))
+(flet ($e137 (bvuge v2 (zero_extend[1] ?e68)))
+(flet ($e138 (bvsle (sign_extend[11] ?e44) ?e39))
+(flet ($e139 (bvule (sign_extend[4] ?e13) ?e36))
+(flet ($e140 (bvslt ?e38 (zero_extend[15] ?e64)))
+(flet ($e141 (bvsge (sign_extend[5] ?e64) ?e14))
+(flet ($e142 (bvsge (sign_extend[10] ?e61) ?e65))
+(flet ($e143 (bvslt (zero_extend[3] ?e51) ?e13))
+(flet ($e144 (distinct ?e83 (sign_extend[10] ?e81)))
+(flet ($e145 (bvsle (zero_extend[10] ?e66) ?e83))
+(flet ($e146 (bvule (sign_extend[8] ?e61) ?e83))
+(flet ($e147 (bvule (zero_extend[5] ?e16) ?e55))
+(flet ($e148 (bvuge ?e83 (sign_extend[2] ?e25)))
+(flet ($e149 (bvule ?e50 (sign_extend[2] ?e32)))
+(flet ($e150 (= (sign_extend[1] ?e37) v0))
+(flet ($e151 (bvugt (sign_extend[5] v3) ?e45))
+(flet ($e152 (bvugt ?e55 (sign_extend[8] ?e14)))
+(flet ($e153 (bvsle (zero_extend[13] ?e78) ?e74))
+(flet ($e154 (bvule ?e61 (sign_extend[2] ?e73)))
+(flet ($e155 (bvule ?e22 ?e57))
+(flet ($e156 (bvugt ?e78 ?e32))
+(flet ($e157 (bvuge ?e65 ?e60))
+(flet ($e158 (distinct ?e52 (sign_extend[10] ?e14)))
+(flet ($e159 (bvsge ?e24 ?e43))
+(flet ($e160 (bvsge ?e25 (sign_extend[2] ?e26)))
+(flet ($e161 (bvsgt v0 (zero_extend[9] ?e17)))
+(flet ($e162 (bvult ?e18 ?e72))
+(flet ($e163 (bvsgt ?e53 (sign_extend[3] ?e21)))
+(flet ($e164 (bvsgt ?e77 (sign_extend[2] ?e85)))
+(flet ($e165 (distinct (sign_extend[15] ?e62) ?e38))
+(flet ($e166 (bvsle ?e50 ?e44))
+(flet ($e167 (bvuge ?e39 (zero_extend[1] ?e65)))
+(flet ($e168 (bvsgt v4 (sign_extend[10] ?e85)))
+(flet ($e169 (= (sign_extend[5] ?e68) ?e55))
+(flet ($e170 (= (zero_extend[5] ?e16) ?e67))
+(flet ($e171 (distinct ?e53 (sign_extend[12] ?e32)))
+(flet ($e172 (bvule ?e58 ?e72))
+(flet ($e173 (bvsgt v2 (sign_extend[9] ?e32)))
+(flet ($e174 (bvuge ?e59 (sign_extend[2] ?e15)))
+(flet ($e175 (distinct (zero_extend[8] ?e63) ?e25))
+(flet ($e176 (bvslt (sign_extend[4] ?e59) ?e45))
+(flet ($e177 (bvule v0 (zero_extend[5] ?e25)))
+(flet ($e178 (bvslt ?e25 (zero_extend[4] ?e17)))
+(flet ($e179 (bvule (sign_extend[13] ?e85) ?e70))
+(flet ($e180 (bvsge ?e26 ?e26))
+(flet ($e181 (bvsgt ?e86 (zero_extend[4] ?e54)))
+(flet ($e182 (bvsle (sign_extend[9] ?e57) v2))
+(flet ($e183 (bvuge ?e86 (sign_extend[13] ?e80)))
+(flet ($e184 (distinct ?e38 (sign_extend[2] ?e43)))
+(flet ($e185 (bvugt ?e74 ?e39))
+(flet ($e186 (bvsge ?e56 (sign_extend[3] ?e13)))
+(flet ($e187 (bvsge ?e32 ?e76))
+(flet ($e188 (bvugt ?e36 ?e36))
+(flet ($e189 (distinct (zero_extend[6] ?e17) ?e82))
+(flet ($e190 (bvsle ?e67 (zero_extend[5] ?e59)))
+(flet ($e191 (bvugt ?e51 (zero_extend[2] ?e17)))
+(flet ($e192 (= ?e51 (sign_extend[6] ?e18)))
+(flet ($e193 (bvsge ?e81 ?e32))
+(flet ($e194 (bvuge (zero_extend[4] v2) ?e84))
+(flet ($e195 (= ?e43 (zero_extend[9] ?e17)))
+(flet ($e196 (bvsgt ?e74 (zero_extend[11] ?e77)))
+(flet ($e197 (bvugt ?e83 (sign_extend[10] ?e78)))
+(flet ($e198 (bvsgt ?e25 (zero_extend[1] v3)))
+(flet ($e199 (bvsge (sign_extend[7] ?e32) v3))
+(flet ($e200 (bvuge ?e39 (zero_extend[13] ?e64)))
+(flet ($e201 (bvsgt ?e65 (sign_extend[12] ?e32)))
+(flet ($e202 (bvuge ?e45 ?e60))
+(flet ($e203 (distinct ?e59 (sign_extend[8] ?e62)))
+(flet ($e204 (bvsle (sign_extend[4] ?e47) ?e15))
+(flet ($e205 (bvsle (zero_extend[8] ?e81) ?e16))
+(flet ($e206 (bvugt ?e16 (sign_extend[4] ?e17)))
+(flet ($e207 (bvule ?e77 (zero_extend[2] ?e64)))
+(flet ($e208 (bvule ?e64 ?e19))
+(flet ($e209 (bvule ?e86 ?e43))
+(flet ($e210 (bvsgt (zero_extend[1] ?e60) ?e55))
+(flet ($e211 (bvsle (sign_extend[2] ?e19) ?e47))
+(flet ($e212 (bvuge v0 (sign_extend[1] ?e65)))
+(flet ($e213 (bvult (zero_extend[9] ?e18) ?e13))
+(flet ($e214 (distinct ?e35 (sign_extend[13] ?e32)))
+(flet ($e215 (distinct (zero_extend[2] ?e58) ?e47))
+(flet ($e216 (bvsge (zero_extend[1] ?e56) ?e43))
+(flet ($e217 (bvslt ?e81 ?e19))
+(flet ($e218 (distinct (sign_extend[6] ?e20) ?e35))
+(flet ($e219 (bvsgt (sign_extend[2] ?e67) ?e52))
+(flet ($e220 (bvsgt (zero_extend[2] ?e82) ?e56))
+(flet ($e221 (bvule ?e77 (zero_extend[2] ?e19)))
+(flet ($e222 (bvuge ?e65 (zero_extend[6] ?e51)))
+(flet ($e223 (bvuge ?e47 ?e34))
+(flet ($e224 (bvult ?e38 (sign_extend[15] ?e85)))
+(flet ($e225 (bvsgt v4 (zero_extend[10] ?e78)))
+(flet ($e226 (bvugt (sign_extend[11] ?e17) ?e38))
+(flet ($e227 (bvult (zero_extend[2] ?e69) ?e77))
+(flet ($e228 (bvuge ?e39 (sign_extend[13] ?e63)))
+(flet ($e229 (distinct (zero_extend[13] ?e85) ?e39))
+(flet ($e230 (bvsgt (zero_extend[12] ?e57) ?e60))
+(flet ($e231 (bvugt ?e71 (sign_extend[2] ?e18)))
+(flet ($e232 (= (zero_extend[4] ?e50) ?e26))
+(flet ($e233 (bvuge ?e70 (zero_extend[13] ?e22)))
+(flet ($e234 (bvsgt v2 (sign_extend[9] ?e19)))
+(flet ($e235 (bvuge (sign_extend[13] ?e22) ?e39))
+(flet ($e236 (bvuge (sign_extend[7] ?e51) ?e70))
+(flet ($e237 (bvslt ?e18 ?e73))
+(flet ($e238 (bvult ?e54 (sign_extend[9] ?e78)))
+(flet ($e239 (bvuge v2 (sign_extend[1] ?e25)))
+(flet ($e240 (= ?e21 (sign_extend[9] ?e85)))
+(flet ($e241 (bvsle v3 (zero_extend[7] ?e62)))
+(flet ($e242 (= ?e71 (sign_extend[2] ?e63)))
+(flet ($e243 (bvsgt ?e45 (zero_extend[12] ?e85)))
+(flet ($e244 (bvsle ?e55 (zero_extend[13] ?e48)))
+(flet ($e245 (= ?e30 ?e30))
+(flet ($e246 (and $e97 $e119))
+(flet ($e247 (if_then_else $e217 $e186 $e127))
+(flet ($e248 (iff $e99 $e89))
+(flet ($e249 (implies $e241 $e226))
+(flet ($e250 (implies $e102 $e114))
+(flet ($e251 (if_then_else $e236 $e117 $e184))
+(flet ($e252 (if_then_else $e111 $e138 $e219))
+(flet ($e253 (or $e227 $e135))
+(flet ($e254 (xor $e93 $e221))
+(flet ($e255 (and $e104 $e210))
+(flet ($e256 (if_then_else $e158 $e238 $e172))
+(flet ($e257 (and $e113 $e136))
+(flet ($e258 (not $e190))
+(flet ($e259 (implies $e163 $e94))
+(flet ($e260 (iff $e243 $e228))
+(flet ($e261 (not $e155))
+(flet ($e262 (if_then_else $e147 $e141 $e216))
+(flet ($e263 (xor $e194 $e160))
+(flet ($e264 (or $e103 $e233))
+(flet ($e265 (and $e179 $e140))
+(flet ($e266 (if_then_else $e173 $e198 $e150))
+(flet ($e267 (xor $e167 $e231))
+(flet ($e268 (if_then_else $e223 $e252 $e258))
+(flet ($e269 (iff $e177 $e200))
+(flet ($e270 (or $e245 $e132))
+(flet ($e271 (implies $e148 $e218))
+(flet ($e272 (or $e265 $e195))
+(flet ($e273 (not $e96))
+(flet ($e274 (or $e123 $e182))
+(flet ($e275 (if_then_else $e239 $e193 $e178))
+(flet ($e276 (xor $e249 $e110))
+(flet ($e277 (xor $e251 $e264))
+(flet ($e278 (if_then_else $e181 $e222 $e244))
+(flet ($e279 (if_then_else $e207 $e128 $e152))
+(flet ($e280 (not $e274))
+(flet ($e281 (if_then_else $e92 $e255 $e214))
+(flet ($e282 (iff $e234 $e115))
+(flet ($e283 (xor $e260 $e209))
+(flet ($e284 (and $e191 $e180))
+(flet ($e285 (or $e183 $e95))
+(flet ($e286 (or $e259 $e100))
+(flet ($e287 (if_then_else $e273 $e153 $e101))
+(flet ($e288 (not $e188))
+(flet ($e289 (not $e229))
+(flet ($e290 (iff $e284 $e268))
+(flet ($e291 (or $e269 $e124))
+(flet ($e292 (or $e202 $e145))
+(flet ($e293 (or $e169 $e129))
+(flet ($e294 (iff $e204 $e142))
+(flet ($e295 (and $e271 $e146))
+(flet ($e296 (implies $e185 $e144))
+(flet ($e297 (iff $e118 $e143))
+(flet ($e298 (and $e242 $e263))
+(flet ($e299 (or $e283 $e125))
+(flet ($e300 (xor $e130 $e168))
+(flet ($e301 (if_then_else $e213 $e257 $e293))
+(flet ($e302 (xor $e277 $e280))
+(flet ($e303 (or $e199 $e187))
+(flet ($e304 (and $e109 $e237))
+(flet ($e305 (implies $e165 $e205))
+(flet ($e306 (xor $e91 $e299))
+(flet ($e307 (or $e246 $e175))
+(flet ($e308 (implies $e133 $e302))
+(flet ($e309 (xor $e307 $e174))
+(flet ($e310 (or $e261 $e298))
+(flet ($e311 (iff $e297 $e122))
+(flet ($e312 (xor $e267 $e170))
+(flet ($e313 (iff $e292 $e300))
+(flet ($e314 (implies $e256 $e287))
+(flet ($e315 (and $e201 $e120))
+(flet ($e316 (and $e106 $e304))
+(flet ($e317 (or $e126 $e290))
+(flet ($e318 (implies $e262 $e108))
+(flet ($e319 (and $e107 $e310))
+(flet ($e320 (implies $e220 $e206))
+(flet ($e321 (iff $e196 $e225))
+(flet ($e322 (xor $e295 $e294))
+(flet ($e323 (xor $e87 $e321))
+(flet ($e324 (and $e240 $e151))
+(flet ($e325 (xor $e121 $e161))
+(flet ($e326 (iff $e90 $e319))
+(flet ($e327 (iff $e215 $e248))
+(flet ($e328 (xor $e285 $e288))
+(flet ($e329 (or $e232 $e98))
+(flet ($e330 (not $e317))
+(flet ($e331 (and $e315 $e270))
+(flet ($e332 (iff $e318 $e279))
+(flet ($e333 (or $e328 $e253))
+(flet ($e334 (xor $e276 $e306))
+(flet ($e335 (iff $e88 $e235))
+(flet ($e336 (xor $e211 $e313))
+(flet ($e337 (iff $e286 $e324))
+(flet ($e338 (implies $e266 $e166))
+(flet ($e339 (if_then_else $e250 $e312 $e212))
+(flet ($e340 (not $e131))
+(flet ($e341 (xor $e329 $e275))
+(flet ($e342 (iff $e208 $e289))
+(flet ($e343 (and $e338 $e154))
+(flet ($e344 (not $e149))
+(flet ($e345 (and $e134 $e272))
+(flet ($e346 (implies $e301 $e322))
+(flet ($e347 (and $e346 $e176))
+(flet ($e348 (not $e343))
+(flet ($e349 (xor $e316 $e308))
+(flet ($e350 (or $e281 $e281))
+(flet ($e351 (not $e333))
+(flet ($e352 (implies $e351 $e327))
+(flet ($e353 (xor $e345 $e112))
+(flet ($e354 (xor $e311 $e157))
+(flet ($e355 (implies $e350 $e341))
+(flet ($e356 (implies $e344 $e171))
+(flet ($e357 (implies $e326 $e347))
+(flet ($e358 (implies $e332 $e162))
+(flet ($e359 (iff $e320 $e342))
+(flet ($e360 (iff $e159 $e339))
+(flet ($e361 (if_then_else $e337 $e334 $e358))
+(flet ($e362 (iff $e116 $e224))
+(flet ($e363 (or $e278 $e197))
+(flet ($e364 (if_then_else $e137 $e362 $e296))
+(flet ($e365 (or $e336 $e323))
+(flet ($e366 (and $e356 $e330))
+(flet ($e367 (implies $e230 $e348))
+(flet ($e368 (not $e365))
+(flet ($e369 (iff $e352 $e353))
+(flet ($e370 (or $e189 $e354))
+(flet ($e371 (and $e331 $e139))
+(flet ($e372 (not $e254))
+(flet ($e373 (implies $e370 $e291))
+(flet ($e374 (xor $e349 $e367))
+(flet ($e375 (iff $e305 $e361))
+(flet ($e376 (not $e364))
+(flet ($e377 (if_then_else $e314 $e340 $e309))
+(flet ($e378 (iff $e335 $e357))
+(flet ($e379 (xor $e355 $e366))
+(flet ($e380 (or $e359 $e359))
+(flet ($e381 (implies $e375 $e105))
+(flet ($e382 (if_then_else $e203 $e380 $e164))
+(flet ($e383 (implies $e371 $e325))
+(flet ($e384 (implies $e282 $e360))
+(flet ($e385 (xor $e376 $e373))
+(flet ($e386 (not $e363))
+(flet ($e387 (implies $e247 $e383))
+(flet ($e388 (implies $e378 $e156))
+(flet ($e389 (implies $e382 $e369))
+(flet ($e390 (not $e386))
+(flet ($e391 (not $e389))
+(flet ($e392 (implies $e379 $e384))
+(flet ($e393 (iff $e381 $e192))
+(flet ($e394 (if_then_else $e385 $e388 $e374))
+(flet ($e395 (not $e377))
+(flet ($e396 (if_then_else $e390 $e387 $e387))
+(flet ($e397 (if_then_else $e394 $e396 $e396))
+(flet ($e398 (implies $e303 $e392))
+(flet ($e399 (or $e397 $e398))
+(flet ($e400 (implies $e399 $e368))
+(flet ($e401 (implies $e391 $e372))
+(flet ($e402 (and $e400 $e393))
+(flet ($e403 (if_then_else $e401 $e395 $e402))
+$e403
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+