missing problems

diff --git a/test/regress/regress0/aufbv/fuzz03.delta01.smt b/test/regress/regress0/aufbv/fuzz03.delta01.smt
new file mode 100644 (file)
index 0000000..f1abfed
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz03.delta01.smt
@@ -0,0 +1,52 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((a8 Array[14:12]))
+:extrafuns ((v1 BitVec[5]))
+:status sat
+:formula
+(let (?n1 bv1[14])
+(let (?n2 bv1[12])
+(let (?n3 (store a8 ?n1 ?n2))
+(flet ($n4 (bvugt v1 v1))
+(let (?n5 bv1[1])
+(let (?n6 bv0[1])
+(let (?n7 (ite $n4 ?n5 ?n6))
+(let (?n8 (sign_extend[13] ?n7))
+(let (?n9 (store ?n3 ?n8 ?n2))
+(let (?n10 bv0[12])
+(let (?n11 (store ?n9 ?n1 ?n10))
+(let (?n12 bv0[14])
+(let (?n13 (select ?n3 ?n12))
+(let (?n14 (zero_extend[2] ?n13))
+(let (?n15 (store ?n11 ?n14 ?n10))
+(let (?n16 (select ?n15 ?n12))
+(flet ($n17 (bvsgt ?n16 ?n10))
+(let (?n18 (bvnor ?n2 ?n10))
+(let (?n19 (zero_extend[2] ?n18))
+(let (?n20 (store ?n9 ?n19 ?n10))
+(flet ($n21 (= a8 ?n9))
+(let (?n22 (ite $n21 ?n5 ?n6))
+(let (?n23 (sign_extend[13] ?n22))
+(let (?n24 (select ?n20 ?n23))
+(let (?n25 (zero_extend[2] ?n24))
+(let (?n26 (select ?n3 ?n25))
+(flet ($n27 (bvuge ?n10 ?n26))
+(flet ($n28 (= ?n9 ?n15))
+(flet ($n29 false)
+(flet ($n30 (bvsle ?n24 ?n10))
+(flet ($n31 (if_then_else $n28 $n29 $n30))
+(let (?n32 (sign_extend[11] ?n5))
+(flet ($n33 (= ?n9 ?n20))
+(let (?n34 (ite $n33 ?n5 ?n6))
+(let (?n35 (sign_extend[13] ?n34))
+(let (?n36 (select ?n3 ?n35))
+(let (?n37 (bvor ?n18 ?n36))
+(flet ($n38 (bvsge ?n32 ?n37))
+(flet ($n39 (if_then_else $n31 $n38 $n31))
+(flet ($n40 (implies $n27 $n39))
+(let (?n41 (store a8 ?n12 ?n10))
+(flet ($n42 (= ?n3 ?n41))
+(flet ($n43 (or $n40 $n42))
+(flet ($n44 (implies $n17 $n43))
+$n44
+)))))))))))))))))))))))))))))))))))))))))))))

diff --git a/test/regress/regress0/aufbv/fuzz03.smt b/test/regress/regress0/aufbv/fuzz03.smt
new file mode 100644 (file)
index 0000000..1bbc671
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz03.smt
@@ -0,0 +1,501 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status sat
+:extrafuns ((v0 BitVec[15]))
+:extrafuns ((v1 BitVec[5]))
+:extrafuns ((a2 Array[2:16]))
+:extrafuns ((a3 Array[5:1]))
+:extrafuns ((a4 Array[16:14]))
+:extrafuns ((a5 Array[12:2]))
+:extrafuns ((a6 Array[1:4]))
+:extrafuns ((a7 Array[12:16]))
+:extrafuns ((a8 Array[14:12]))
+:extrafuns ((a9 Array[7:7]))
+:formula
+(let (?e10 bv0[4])
+(let (?e11 bv519[12])
+(let (?e12 bv15320[15])
+(let (?e13 bv56[6])
+(let (?e14 bv583[13])
+(let (?e15 (ite (bvugt v1 v1) bv1[1] bv0[1]))
+(let (?e16 (rotate_right[8] ?e14))
+(let (?e17 (rotate_left[5] ?e11))
+(let (?e18 (zero_extend[0] ?e13))
+(let (?e19 (rotate_right[2] ?e10))
+(let (?e20 (sign_extend[12] ?e15))
+(let (?e21 (bvnor (zero_extend[8] ?e10) ?e17))
+(let (?e22 (bvxnor v0 (zero_extend[2] ?e20)))
+(let (?e23 (rotate_right[1] ?e19))
+(let (?e24 (bvneg ?e12))
+(let (?e25 (store a8 (zero_extend[2] ?e11) ?e17))
+(let (?e26 (store a5 (sign_extend[8] ?e10) (extract[1:0] ?e16)))
+(let (?e27 (store ?e25 (sign_extend[13] ?e15) (sign_extend[6] ?e18)))
+(let (?e28 (store ?e27 (sign_extend[2] ?e11) (extract[14:3] ?e12)))
+(let (?e29 (store ?e27 (zero_extend[2] ?e21) (extract[12:1] ?e16)))
+(let (?e30 (ite (= ?e27 a8) bv1[1] bv0[1]))
+(let (?e31 (ite (= ?e27 ?e29) bv1[1] bv0[1]))
+(let (?e32 (select a3 (zero_extend[4] ?e15)))
+(let (?e33 (select a4 (sign_extend[1] v0)))
+(let (?e34 (select ?e29 (sign_extend[13] ?e30)))
+(let (?e35 (select ?e25 (sign_extend[13] ?e31)))
+(let (?e36 (select ?e25 (sign_extend[10] ?e23)))
+(let (?e37 (select a8 (sign_extend[10] ?e10)))
+(let (?e38 (store a6 (extract[11:11] ?e11) ?e10))
+(let (?e39 (store ?e28 (zero_extend[2] ?e36) (sign_extend[8] ?e10)))
+(let (?e40 (store a8 (sign_extend[1] ?e20) (zero_extend[8] ?e19)))
+(let (?e41 (ite (= a8 ?e29) bv1[1] bv0[1]))
+(let (?e42 (select ?e39 (sign_extend[1] ?e20)))
+(let (?e43 (select ?e40 (zero_extend[2] ?e17)))
+(let (?e44 (select a2 (extract[8:7] v0)))
+(let (?e45 (store ?e29 (zero_extend[1] ?e16) (extract[11:0] v0)))
+(let (?e46 (select ?e27 (zero_extend[13] ?e32)))
+(let (?e47 (select ?e28 (zero_extend[13] ?e31)))
+(let (?e48 (store a4 (zero_extend[10] ?e18) ?e33))
+(let (?e49 (select ?e25 (zero_extend[2] ?e34)))
+(let (?e50 (ite (bvsge (zero_extend[14] ?e32) ?e22) bv1[1] bv0[1]))
+(let (?e51 (bvand ?e19 ?e10))
+(let (?e52 (ite (bvslt ?e43 (zero_extend[11] ?e50)) bv1[1] bv0[1]))
+(let (?e53 (bvashr ?e11 ?e42))
+(let (?e54 (bvcomp (sign_extend[12] ?e30) ?e14))
+(let (?e55 (bvor ?e13 ?e13))
+(let (?e56 (bvneg ?e21))
+(let (?e57 (repeat[1] ?e56))
+(let (?e58 (bvcomp (zero_extend[3] ?e17) ?e22))
+(let (?e59 (bvnand ?e21 (sign_extend[11] ?e50)))
+(let (?e60 (ite (= bv1[1] (extract[0:0] ?e15)) ?e57 ?e11))
+(let (?e61 (extract[9:9] ?e20))
+(let (?e62 (extract[10:8] v0))
+(let (?e63 (concat ?e47 ?e41))
+(let (?e64 (extract[8:7] ?e33))
+(let (?e65 (bvand (sign_extend[1] ?e37) ?e16))
+(let (?e66 (ite (= ?e44 (sign_extend[15] ?e58)) bv1[1] bv0[1]))
+(let (?e67 (bvashr (zero_extend[7] v1) ?e34))
+(let (?e68 (ite (bvuge ?e59 (zero_extend[11] ?e58)) bv1[1] bv0[1]))
+(let (?e69 (bvor ?e35 ?e21))
+(let (?e70 (bvashr (sign_extend[8] ?e23) ?e36))
+(let (?e71 (sign_extend[3] ?e51))
+(let (?e72 (bvxnor ?e13 (zero_extend[5] ?e50)))
+(let (?e73 (rotate_right[5] ?e34))
+(let (?e74 (bvxnor ?e41 ?e68))
+(let (?e75 (rotate_right[0] ?e12))
+(let (?e76 (ite (bvslt (zero_extend[14] ?e31) ?e75) bv1[1] bv0[1]))
+(let (?e77 (ite (bvuge ?e18 ?e72) bv1[1] bv0[1]))
+(let (?e78 (ite (bvsle ?e60 (zero_extend[10] ?e64)) bv1[1] bv0[1]))
+(let (?e79 (ite (bvugt (zero_extend[11] ?e66) ?e67) bv1[1] bv0[1]))
+(let (?e80 (ite (bvult (zero_extend[11] ?e31) ?e43) bv1[1] bv0[1]))
+(let (?e81 (bvshl ?e49 (sign_extend[11] ?e41)))
+(let (?e82 (ite (bvsle (sign_extend[1] ?e37) ?e20) bv1[1] bv0[1]))
+(let (?e83 (bvnot ?e30))
+(let (?e84 (bvmul ?e36 ?e42))
+(let (?e85 (bvand ?e46 (sign_extend[11] ?e31)))
+(let (?e86 (bvadd ?e12 (sign_extend[9] ?e18)))
+(let (?e87 (bvshl ?e35 ?e36))
+(let (?e88 (bvxor ?e73 ?e17))
+(let (?e89 (ite (= bv1[1] (extract[3:3] ?e22)) ?e70 (sign_extend[11] ?e82)))
+(let (?e90 (bvmul ?e14 (sign_extend[12] ?e30)))
+(let (?e91 (bvnor ?e90 (sign_extend[11] ?e64)))
+(let (?e92 (bvnand ?e37 ?e70))
+(let (?e93 (ite (= ?e65 (zero_extend[1] ?e87)) bv1[1] bv0[1]))
+(let (?e94 (sign_extend[0] ?e64))
+(let (?e95 (bvnot ?e24))
+(flet ($e96 (bvslt (zero_extend[11] ?e52) ?e67))
+(flet ($e97 (distinct ?e21 ?e67))
+(flet ($e98 (distinct (sign_extend[5] ?e93) ?e18))
+(flet ($e99 (distinct (zero_extend[3] ?e42) ?e95))
+(flet ($e100 (bvugt (zero_extend[6] ?e72) ?e17))
+(flet ($e101 (= ?e43 (zero_extend[11] ?e93)))
+(flet ($e102 (bvslt (zero_extend[11] ?e58) ?e85))
+(flet ($e103 (bvugt (sign_extend[14] ?e74) ?e22))
+(flet ($e104 (bvule (zero_extend[6] ?e76) ?e71))
+(flet ($e105 (bvsgt (zero_extend[3] ?e79) ?e23))
+(flet ($e106 (bvsge (zero_extend[3] ?e58) ?e10))
+(flet ($e107 (= ?e59 ?e60))
+(flet ($e108 (bvule (sign_extend[11] ?e15) ?e87))
+(flet ($e109 (bvslt ?e63 (zero_extend[10] ?e62)))
+(flet ($e110 (bvult ?e90 (sign_extend[12] ?e31)))
+(flet ($e111 (distinct (zero_extend[5] ?e74) ?e13))
+(flet ($e112 (distinct ?e74 ?e74))
+(flet ($e113 (distinct ?e20 (sign_extend[7] ?e72)))
+(flet ($e114 (bvsle ?e82 ?e68))
+(flet ($e115 (bvuge ?e14 (sign_extend[1] ?e67)))
+(flet ($e116 (distinct ?e84 ?e59))
+(flet ($e117 (bvsle ?e46 ?e60))
+(flet ($e118 (bvsle ?e15 ?e74))
+(flet ($e119 (bvslt v0 (zero_extend[3] ?e88)))
+(flet ($e120 (bvule (zero_extend[5] ?e58) ?e13))
+(flet ($e121 (bvugt (sign_extend[8] ?e19) ?e47))
+(flet ($e122 (bvult ?e63 (sign_extend[1] ?e87)))
+(flet ($e123 (bvslt ?e91 (zero_extend[12] ?e66)))
+(flet ($e124 (bvule (sign_extend[11] ?e80) ?e36))
+(flet ($e125 (bvule ?e60 ?e42))
+(flet ($e126 (bvuge (sign_extend[11] ?e52) ?e11))
+(flet ($e127 (bvslt ?e22 (zero_extend[2] ?e63)))
+(flet ($e128 (bvsge (zero_extend[12] ?e15) ?e90))
+(flet ($e129 (bvsle (zero_extend[1] ?e37) ?e16))
+(flet ($e130 (bvslt ?e34 (zero_extend[11] ?e79)))
+(flet ($e131 (bvuge (sign_extend[11] ?e32) ?e67))
+(flet ($e132 (distinct (sign_extend[13] ?e54) ?e33))
+(flet ($e133 (bvuge ?e61 ?e76))
+(flet ($e134 (bvsge ?e62 (sign_extend[2] ?e32)))
+(flet ($e135 (bvsgt ?e88 (zero_extend[11] ?e50)))
+(flet ($e136 (distinct ?e56 (sign_extend[8] ?e10)))
+(flet ($e137 (bvslt ?e61 ?e80))
+(flet ($e138 (bvsle (zero_extend[12] ?e82) ?e65))
+(flet ($e139 (bvuge ?e11 (sign_extend[11] ?e82)))
+(flet ($e140 (bvslt (sign_extend[6] ?e55) ?e67))
+(flet ($e141 (bvule ?e95 (zero_extend[3] ?e81)))
+(flet ($e142 (bvult ?e34 (sign_extend[6] ?e55)))
+(flet ($e143 (bvuge (sign_extend[14] ?e52) ?e86))
+(flet ($e144 (bvsge ?e92 ?e60))
+(flet ($e145 (bvule ?e13 (sign_extend[1] v1)))
+(flet ($e146 (distinct (sign_extend[3] ?e32) ?e23))
+(flet ($e147 (distinct ?e69 ?e17))
+(flet ($e148 (bvult (zero_extend[11] ?e54) ?e53))
+(flet ($e149 (distinct (sign_extend[8] ?e10) ?e36))
+(flet ($e150 (bvuge (zero_extend[1] ?e58) ?e94))
+(flet ($e151 (= ?e47 (zero_extend[11] ?e83)))
+(flet ($e152 (bvsgt ?e42 (zero_extend[11] ?e32)))
+(flet ($e153 (distinct ?e91 (sign_extend[1] ?e87)))
+(flet ($e154 (bvugt (zero_extend[6] ?e13) ?e87))
+(flet ($e155 (bvsge (sign_extend[11] ?e76) ?e69))
+(flet ($e156 (bvsge ?e69 ?e53))
+(flet ($e157 (bvugt ?e11 ?e46))
+(flet ($e158 (distinct (sign_extend[5] ?e71) ?e85))
+(flet ($e159 (bvuge ?e75 (zero_extend[14] ?e31)))
+(flet ($e160 (bvugt (zero_extend[11] ?e76) ?e42))
+(flet ($e161 (bvsgt ?e12 (zero_extend[14] ?e31)))
+(flet ($e162 (bvule ?e66 ?e82))
+(flet ($e163 (bvsle ?e86 (zero_extend[11] ?e51)))
+(flet ($e164 (distinct ?e85 (sign_extend[11] ?e58)))
+(flet ($e165 (bvugt ?e14 (sign_extend[1] ?e56)))
+(flet ($e166 (bvslt (zero_extend[8] ?e23) ?e36))
+(flet ($e167 (bvuge ?e69 ?e60))
+(flet ($e168 (bvult (sign_extend[12] ?e62) ?e24))
+(flet ($e169 (bvsle (zero_extend[4] ?e81) ?e44))
+(flet ($e170 (bvslt (sign_extend[3] ?e58) ?e51))
+(flet ($e171 (bvuge (sign_extend[4] ?e73) ?e44))
+(flet ($e172 (bvult ?e37 (zero_extend[8] ?e51)))
+(flet ($e173 (bvsle (sign_extend[1] ?e81) ?e90))
+(flet ($e174 (bvslt ?e49 (zero_extend[7] v1)))
+(flet ($e175 (bvsge (sign_extend[6] ?e93) ?e71))
+(flet ($e176 (bvuge (zero_extend[15] ?e61) ?e44))
+(flet ($e177 (bvslt ?e37 (zero_extend[5] ?e71)))
+(flet ($e178 (bvuge (sign_extend[1] ?e10) v1))
+(flet ($e179 (bvslt (zero_extend[3] ?e89) ?e22))
+(flet ($e180 (bvuge (zero_extend[12] ?e77) ?e65))
+(flet ($e181 (bvsle (sign_extend[9] ?e13) ?e12))
+(flet ($e182 (bvsle ?e87 (zero_extend[10] ?e64)))
+(flet ($e183 (= (zero_extend[3] ?e91) ?e44))
+(flet ($e184 (bvule ?e65 (sign_extend[9] ?e19)))
+(flet ($e185 (bvsle ?e24 (zero_extend[3] ?e67)))
+(flet ($e186 (bvslt ?e91 (sign_extend[1] ?e67)))
+(flet ($e187 (bvuge ?e42 ?e56))
+(flet ($e188 (bvult ?e85 (zero_extend[11] ?e83)))
+(flet ($e189 (bvule ?e47 ?e92))
+(flet ($e190 (= (zero_extend[1] ?e92) ?e20))
+(flet ($e191 (bvuge (zero_extend[8] ?e51) ?e36))
+(flet ($e192 (bvsgt ?e12 (zero_extend[9] ?e18)))
+(flet ($e193 (bvule (sign_extend[12] ?e94) ?e33))
+(flet ($e194 (distinct ?e46 (zero_extend[11] ?e31)))
+(flet ($e195 (bvult (sign_extend[13] ?e94) ?e86))
+(flet ($e196 (bvslt ?e12 (sign_extend[14] ?e80)))
+(flet ($e197 (bvsgt ?e13 (zero_extend[5] ?e58)))
+(flet ($e198 (bvule (sign_extend[3] ?e53) ?e12))
+(flet ($e199 (bvslt ?e86 (zero_extend[3] ?e36)))
+(flet ($e200 (bvslt (zero_extend[11] ?e19) ?e86))
+(flet ($e201 (distinct (zero_extend[3] ?e73) ?e75))
+(flet ($e202 (bvuge ?e88 ?e85))
+(flet ($e203 (bvult (sign_extend[14] ?e31) ?e75))
+(flet ($e204 (bvugt ?e90 (sign_extend[7] ?e13)))
+(flet ($e205 (bvsle (zero_extend[1] ?e36) ?e91))
+(flet ($e206 (bvuge ?e56 ?e49))
+(flet ($e207 (bvugt ?e37 (zero_extend[11] ?e52)))
+(flet ($e208 (bvsgt ?e42 (zero_extend[11] ?e82)))
+(flet ($e209 (bvugt ?e21 ?e21))
+(flet ($e210 (bvsle ?e60 ?e85))
+(flet ($e211 (bvugt (zero_extend[11] ?e30) ?e35))
+(flet ($e212 (bvsle ?e17 ?e89))
+(flet ($e213 (bvsgt ?e42 ?e37))
+(flet ($e214 (bvsle ?e34 (sign_extend[8] ?e51)))
+(flet ($e215 (bvugt (zero_extend[3] ?e83) ?e23))
+(flet ($e216 (bvuge ?e64 (zero_extend[1] ?e79)))
+(flet ($e217 (= ?e22 (sign_extend[3] ?e70)))
+(flet ($e218 (= ?e67 (zero_extend[11] ?e78)))
+(flet ($e219 (= ?e55 (zero_extend[5] ?e79)))
+(flet ($e220 (= (sign_extend[11] ?e19) ?e95))
+(flet ($e221 (distinct (zero_extend[3] ?e59) ?e95))
+(flet ($e222 (bvslt (sign_extend[5] ?e54) ?e18))
+(flet ($e223 (bvslt ?e92 ?e67))
+(flet ($e224 (distinct (sign_extend[3] ?e85) ?e24))
+(flet ($e225 (bvult ?e36 (zero_extend[11] ?e82)))
+(flet ($e226 (distinct (zero_extend[11] ?e54) ?e46))
+(flet ($e227 (bvsgt ?e95 (sign_extend[9] ?e72)))
+(flet ($e228 (bvslt ?e90 (zero_extend[12] ?e15)))
+(flet ($e229 (bvuge ?e44 (zero_extend[4] ?e46)))
+(flet ($e230 (bvult ?e57 ?e43))
+(flet ($e231 (bvuge (zero_extend[14] ?e30) ?e24))
+(flet ($e232 (distinct ?e43 ?e73))
+(flet ($e233 (bvsge (sign_extend[2] ?e61) ?e62))
+(flet ($e234 (bvslt ?e56 ?e21))
+(flet ($e235 (bvuge ?e63 (sign_extend[9] ?e10)))
+(flet ($e236 (bvuge ?e95 ?e75))
+(flet ($e237 (bvult (sign_extend[3] ?e74) ?e23))
+(flet ($e238 (bvuge (zero_extend[3] ?e85) ?e86))
+(flet ($e239 (bvult (sign_extend[6] ?e66) ?e71))
+(flet ($e240 (= ?e86 (sign_extend[14] ?e77)))
+(flet ($e241 (bvult (zero_extend[12] ?e52) ?e14))
+(flet ($e242 (distinct (sign_extend[8] ?e19) ?e35))
+(flet ($e243 (bvsgt ?e42 (zero_extend[9] ?e62)))
+(flet ($e244 (bvsgt (sign_extend[2] ?e65) ?e12))
+(flet ($e245 (bvslt ?e16 ?e14))
+(flet ($e246 (bvslt (zero_extend[5] ?e74) ?e55))
+(flet ($e247 (= ?e33 (zero_extend[13] ?e66)))
+(flet ($e248 (bvsle (sign_extend[14] ?e79) ?e95))
+(flet ($e249 (distinct ?e85 ?e70))
+(flet ($e250 (bvsgt ?e88 (sign_extend[6] ?e55)))
+(flet ($e251 (= ?e49 (sign_extend[6] ?e13)))
+(flet ($e252 (bvsle (zero_extend[3] ?e36) ?e24))
+(flet ($e253 (bvugt ?e35 (sign_extend[11] ?e15)))
+(flet ($e254 (= (sign_extend[9] ?e72) ?e75))
+(flet ($e255 (bvsge (sign_extend[5] ?e30) ?e55))
+(flet ($e256 (bvsle (sign_extend[1] ?e92) ?e90))
+(flet ($e257 (bvult ?e91 (zero_extend[12] ?e80)))
+(flet ($e258 (bvugt ?e11 ?e35))
+(flet ($e259 (bvult (sign_extend[8] ?e10) ?e81))
+(flet ($e260 (bvsge ?e85 (zero_extend[6] ?e18)))
+(flet ($e261 (bvslt ?e21 (zero_extend[8] ?e23)))
+(flet ($e262 (bvuge ?e10 (sign_extend[3] ?e52)))
+(flet ($e263 (distinct ?e51 ?e19))
+(flet ($e264 (bvuge (zero_extend[5] ?e71) ?e43))
+(flet ($e265 (bvuge (zero_extend[3] ?e58) ?e10))
+(flet ($e266 (bvuge (zero_extend[9] ?e62) ?e89))
+(flet ($e267 (bvsge ?e46 (zero_extend[10] ?e64)))
+(flet ($e268 (bvsgt ?e95 (zero_extend[3] ?e21)))
+(flet ($e269 (distinct ?e22 (sign_extend[14] ?e30)))
+(flet ($e270 (distinct ?e73 ?e37))
+(flet ($e271 (bvsge (sign_extend[2] ?e34) ?e33))
+(flet ($e272 (bvsgt ?e35 ?e11))
+(flet ($e273 (bvsle ?e60 (sign_extend[11] ?e52)))
+(flet ($e274 (bvsgt (zero_extend[8] ?e23) ?e11))
+(flet ($e275 (bvsgt ?e85 (sign_extend[11] ?e93)))
+(flet ($e276 (= (sign_extend[6] ?e77) ?e71))
+(flet ($e277 (bvule ?e54 ?e68))
+(flet ($e278 (bvule (sign_extend[6] ?e18) ?e49))
+(flet ($e279 (bvslt (zero_extend[4] ?e73) ?e44))
+(flet ($e280 (bvule ?e47 ?e57))
+(flet ($e281 (distinct (zero_extend[1] ?e51) v1))
+(flet ($e282 (bvult (zero_extend[12] ?e77) ?e90))
+(flet ($e283 (bvuge v0 (zero_extend[14] ?e76)))
+(flet ($e284 (= (zero_extend[5] ?e74) ?e18))
+(flet ($e285 (bvugt ?e21 ?e57))
+(flet ($e286 (distinct (sign_extend[2] ?e64) ?e10))
+(flet ($e287 (= (zero_extend[3] ?e64) v1))
+(flet ($e288 (bvsge ?e14 ?e20))
+(flet ($e289 (bvule (zero_extend[3] ?e53) ?e86))
+(flet ($e290 (= ?e73 (sign_extend[11] ?e31)))
+(flet ($e291 (bvsge (zero_extend[12] ?e41) ?e90))
+(flet ($e292 (= ?e27 ?e39))
+(flet ($e293 (= ?e40 ?e25))
+(flet ($e294 (iff $e286 $e100))
+(flet ($e295 (and $e156 $e231))
+(flet ($e296 (implies $e288 $e123))
+(flet ($e297 (not $e243))
+(flet ($e298 (iff $e238 $e146))
+(flet ($e299 (not $e295))
+(flet ($e300 (implies $e107 $e121))
+(flet ($e301 (xor $e250 $e120))
+(flet ($e302 (and $e209 $e296))
+(flet ($e303 (implies $e178 $e167))
+(flet ($e304 (or $e195 $e131))
+(flet ($e305 (implies $e128 $e148))
+(flet ($e306 (or $e223 $e214))
+(flet ($e307 (iff $e136 $e180))
+(flet ($e308 (if_then_else $e132 $e188 $e282))
+(flet ($e309 (not $e101))
+(flet ($e310 (if_then_else $e140 $e142 $e305))
+(flet ($e311 (xor $e242 $e116))
+(flet ($e312 (if_then_else $e114 $e187 $e279))
+(flet ($e313 (implies $e183 $e204))
+(flet ($e314 (iff $e289 $e160))
+(flet ($e315 (not $e97))
+(flet ($e316 (iff $e252 $e273))
+(flet ($e317 (if_then_else $e297 $e245 $e232))
+(flet ($e318 (not $e235))
+(flet ($e319 (xor $e301 $e258))
+(flet ($e320 (or $e254 $e177))
+(flet ($e321 (implies $e230 $e202))
+(flet ($e322 (if_then_else $e175 $e244 $e138))
+(flet ($e323 (and $e302 $e163))
+(flet ($e324 (implies $e113 $e300))
+(flet ($e325 (and $e322 $e211))
+(flet ($e326 (iff $e124 $e278))
+(flet ($e327 (if_then_else $e185 $e221 $e229))
+(flet ($e328 (or $e280 $e251))
+(flet ($e329 (xor $e106 $e226))
+(flet ($e330 (iff $e303 $e308))
+(flet ($e331 (not $e237))
+(flet ($e332 (xor $e111 $e225))
+(flet ($e333 (implies $e155 $e207))
+(flet ($e334 (and $e269 $e317))
+(flet ($e335 (xor $e108 $e133))
+(flet ($e336 (iff $e158 $e172))
+(flet ($e337 (if_then_else $e159 $e323 $e103))
+(flet ($e338 (and $e186 $e104))
+(flet ($e339 (not $e179))
+(flet ($e340 (xor $e304 $e337))
+(flet ($e341 (or $e272 $e293))
+(flet ($e342 (and $e115 $e255))
+(flet ($e343 (and $e198 $e102))
+(flet ($e344 (and $e262 $e343))
+(flet ($e345 (iff $e330 $e336))
+(flet ($e346 (iff $e149 $e122))
+(flet ($e347 (or $e119 $e339))
+(flet ($e348 (or $e222 $e137))
+(flet ($e349 (implies $e319 $e345))
+(flet ($e350 (or $e299 $e117))
+(flet ($e351 (and $e126 $e271))
+(flet ($e352 (xor $e212 $e341))
+(flet ($e353 (if_then_else $e145 $e320 $e265))
+(flet ($e354 (if_then_else $e249 $e268 $e147))
+(flet ($e355 (xor $e331 $e130))
+(flet ($e356 (iff $e274 $e213))
+(flet ($e357 (iff $e246 $e125))
+(flet ($e358 (not $e200))
+(flet ($e359 (if_then_else $e199 $e327 $e355))
+(flet ($e360 (implies $e310 $e354))
+(flet ($e361 (and $e333 $e96))
+(flet ($e362 (and $e318 $e227))
+(flet ($e363 (implies $e321 $e189))
+(flet ($e364 (iff $e247 $e261))
+(flet ($e365 (iff $e351 $e353))
+(flet ($e366 (not $e143))
+(flet ($e367 (and $e256 $e193))
+(flet ($e368 (iff $e340 $e335))
+(flet ($e369 (xor $e118 $e166))
+(flet ($e370 (xor $e357 $e266))
+(flet ($e371 (or $e153 $e157))
+(flet ($e372 (if_then_else $e165 $e240 $e344))
+(flet ($e373 (or $e196 $e342))
+(flet ($e374 (or $e350 $e338))
+(flet ($e375 (not $e315))
+(flet ($e376 (or $e361 $e253))
+(flet ($e377 (xor $e169 $e348))
+(flet ($e378 (not $e373))
+(flet ($e379 (implies $e263 $e311))
+(flet ($e380 (implies $e324 $e135))
+(flet ($e381 (and $e233 $e217))
+(flet ($e382 (implies $e190 $e203))
+(flet ($e383 (if_then_else $e248 $e309 $e224))
+(flet ($e384 (implies $e379 $e349))
+(flet ($e385 (xor $e382 $e292))
+(flet ($e386 (if_then_else $e385 $e257 $e306))
+(flet ($e387 (implies $e380 $e312))
+(flet ($e388 (and $e287 $e161))
+(flet ($e389 (or $e307 $e174))
+(flet ($e390 (implies $e372 $e374))
+(flet ($e391 (implies $e181 $e182))
+(flet ($e392 (iff $e228 $e216))
+(flet ($e393 (and $e141 $e291))
+(flet ($e394 (implies $e367 $e316))
+(flet ($e395 (or $e219 $e368))
+(flet ($e396 (iff $e197 $e236))
+(flet ($e397 (implies $e220 $e326))
+(flet ($e398 (implies $e294 $e260))
+(flet ($e399 (xor $e290 $e285))
+(flet ($e400 (implies $e154 $e154))
+(flet ($e401 (iff $e366 $e396))
+(flet ($e402 (or $e105 $e110))
+(flet ($e403 (xor $e283 $e325))
+(flet ($e404 (iff $e394 $e239))
+(flet ($e405 (iff $e403 $e358))
+(flet ($e406 (xor $e352 $e194))
+(flet ($e407 (or $e378 $e377))
+(flet ($e408 (iff $e388 $e281))
+(flet ($e409 (or $e383 $e171))
+(flet ($e410 (if_then_else $e360 $e402 $e234))
+(flet ($e411 (or $e150 $e264))
+(flet ($e412 (or $e387 $e184))
+(flet ($e413 (if_then_else $e314 $e134 $e392))
+(flet ($e414 (if_then_else $e164 $e267 $e139))
+(flet ($e415 (not $e206))
+(flet ($e416 (not $e277))
+(flet ($e417 (if_then_else $e384 $e276 $e109))
+(flet ($e418 (iff $e389 $e329))
+(flet ($e419 (implies $e410 $e176))
+(flet ($e420 (implies $e418 $e191))
+(flet ($e421 (and $e334 $e170))
+(flet ($e422 (and $e364 $e259))
+(flet ($e423 (and $e412 $e275))
+(flet ($e424 (iff $e404 $e419))
+(flet ($e425 (or $e407 $e129))
+(flet ($e426 (and $e397 $e270))
+(flet ($e427 (not $e313))
+(flet ($e428 (not $e401))
+(flet ($e429 (xor $e152 $e347))
+(flet ($e430 (not $e144))
+(flet ($e431 (and $e201 $e425))
+(flet ($e432 (iff $e431 $e393))
+(flet ($e433 (not $e284))
+(flet ($e434 (or $e328 $e417))
+(flet ($e435 (or $e162 $e428))
+(flet ($e436 (iff $e430 $e390))
+(flet ($e437 (or $e99 $e381))
+(flet ($e438 (if_then_else $e395 $e437 $e356))
+(flet ($e439 (xor $e112 $e432))
+(flet ($e440 (not $e409))
+(flet ($e441 (xor $e415 $e413))
+(flet ($e442 (iff $e359 $e168))
+(flet ($e443 (and $e408 $e436))
+(flet ($e444 (not $e424))
+(flet ($e445 (iff $e414 $e218))
+(flet ($e446 (iff $e405 $e435))
+(flet ($e447 (if_then_else $e440 $e429 $e208))
+(flet ($e448 (not $e439))
+(flet ($e449 (if_then_else $e443 $e416 $e447))
+(flet ($e450 (if_then_else $e438 $e448 $e369))
+(flet ($e451 (xor $e445 $e441))
+(flet ($e452 (and $e375 $e423))
+(flet ($e453 (iff $e451 $e452))
+(flet ($e454 (if_then_else $e363 $e427 $e298))
+(flet ($e455 (iff $e210 $e362))
+(flet ($e456 (implies $e127 $e173))
+(flet ($e457 (not $e192))
+(flet ($e458 (implies $e215 $e411))
+(flet ($e459 (implies $e453 $e433))
+(flet ($e460 (and $e400 $e450))
+(flet ($e461 (iff $e205 $e241))
+(flet ($e462 (and $e399 $e454))
+(flet ($e463 (xor $e98 $e462))
+(flet ($e464 (if_then_else $e370 $e420 $e398))
+(flet ($e465 (xor $e458 $e391))
+(flet ($e466 (and $e365 $e456))
+(flet ($e467 (implies $e455 $e446))
+(flet ($e468 (and $e459 $e442))
+(flet ($e469 (xor $e371 $e457))
+(flet ($e470 (and $e422 $e332))
+(flet ($e471 (implies $e444 $e465))
+(flet ($e472 (not $e421))
+(flet ($e473 (implies $e460 $e406))
+(flet ($e474 (iff $e449 $e469))
+(flet ($e475 (or $e426 $e464))
+(flet ($e476 (and $e376 $e434))
+(flet ($e477 (not $e467))
+(flet ($e478 (not $e475))
+(flet ($e479 (xor $e477 $e346))
+(flet ($e480 (or $e470 $e478))
+(flet ($e481 (implies $e480 $e480))
+(flet ($e482 (and $e481 $e479))
+(flet ($e483 (if_then_else $e461 $e482 $e463))
+(flet ($e484 (and $e386 $e466))
+(flet ($e485 (iff $e483 $e474))
+(flet ($e486 (if_then_else $e484 $e476 $e484))
+(flet ($e487 (iff $e471 $e486))
+(flet ($e488 (not $e151))
+(flet ($e489 (if_then_else $e472 $e488 $e485))
+(flet ($e490 (implies $e468 $e487))
+(flet ($e491 (implies $e473 $e473))
+(flet ($e492 (or $e491 $e490))
+(flet ($e493 (implies $e489 $e492))
+$e493
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+