From b2bafe6e37bf98c8bc640bc0f343a40a11a67dbb Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Tue, 12 Jun 2012 11:35:30 +0000
Subject: [PATCH] wrong answer benchmarks these should be simple constant
 propagation problems

---
 .../regress0/bv/incorrect1.delta01.smt        |  12 +
 test/regress/regress0/bv/incorrect1.smt       | 699 ++++++++++++++++++
 2 files changed, 711 insertions(+)
 create mode 100644 test/regress/regress0/bv/incorrect1.delta01.smt
 create mode 100644 test/regress/regress0/bv/incorrect1.smt

diff --git a/test/regress/regress0/bv/incorrect1.delta01.smt b/test/regress/regress0/bv/incorrect1.delta01.smt
new file mode 100644
index 000000000..e02935bd3
--- /dev/null
+++ b/test/regress/regress0/bv/incorrect1.delta01.smt
@@ -0,0 +1,12 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:status sat
+:formula
+(let (?n1 bv0[9])
+(let (?n2 bv29[5])
+(let (?n3 (sign_extend[4] ?n2))
+(let (?n4 (bvsmod ?n1 ?n3))
+(let (?n5 bv1[9])
+(flet ($n6 (bvult ?n4 ?n5))
+$n6
+)))))))
diff --git a/test/regress/regress0/bv/incorrect1.smt b/test/regress/regress0/bv/incorrect1.smt
new file mode 100644
index 000000000..7df276923
--- /dev/null
+++ b/test/regress/regress0/bv/incorrect1.smt
@@ -0,0 +1,699 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:status unsat
+:extrafuns ((v0 BitVec[8]))
+:extrafuns ((v1 BitVec[14]))
+:formula
+(let (?e2 bv29[5])
+(let (?e3 (bvsrem (sign_extend[3] ?e2) v0))
+(let (?e4 (zero_extend[1] ?e3))
+(let (?e5 (ite (= bv1[1] (extract[1:1] ?e4)) ?e3 v0))
+(let (?e6 (bvor ?e5 (zero_extend[3] ?e2)))
+(let (?e7 (ite (bvugt v0 ?e3) bv1[1] bv0[1]))
+(let (?e8 (bvadd ?e5 ?e5))
+(let (?e9 (bvadd ?e4 (sign_extend[4] ?e2)))
+(let (?e10 (bvmul ?e8 (zero_extend[7] ?e7)))
+(let (?e11 (ite (bvsle (zero_extend[1] ?e5) ?e9) bv1[1] bv0[1]))
+(let (?e12 (ite (bvsle ?e8 v0) bv1[1] bv0[1]))
+(let (?e13 (bvsub ?e6 v0))
+(let (?e14 (bvsmod (sign_extend[1] ?e13) ?e9))
+(let (?e15 (bvashr ?e4 (zero_extend[1] ?e6)))
+(let (?e16 (bvsdiv (zero_extend[7] ?e12) ?e10))
+(let (?e17 (bvneg ?e6))
+(let (?e18 (ite (distinct v0 ?e8) bv1[1] bv0[1]))
+(let (?e19 (ite (bvsge ?e4 (zero_extend[1] ?e16)) bv1[1] bv0[1]))
+(let (?e20 (ite (bvult ?e14 (zero_extend[1] ?e6)) bv1[1] bv0[1]))
+(let (?e21 (zero_extend[12] ?e19))
+(let (?e22 (bvshl ?e7 ?e19))
+(let (?e23 (ite (bvult ?e21 (sign_extend[5] ?e8)) bv1[1] bv0[1]))
+(let (?e24 (ite (bvsge (sign_extend[7] ?e20) ?e13) bv1[1] bv0[1]))
+(let (?e25 (zero_extend[1] ?e3))
+(let (?e26 (bvmul ?e5 ?e13))
+(let (?e27 (ite (bvule (sign_extend[1] ?e8) ?e14) bv1[1] bv0[1]))
+(let (?e28 (bvudiv (sign_extend[7] ?e11) ?e6))
+(let (?e29 (ite (bvult ?e25 (sign_extend[8] ?e11)) bv1[1] bv0[1]))
+(let (?e30 (ite (bvult (sign_extend[7] ?e23) ?e28) bv1[1] bv0[1]))
+(let (?e31 (sign_extend[2] ?e15))
+(let (?e32 (bvsdiv (zero_extend[7] ?e20) ?e17))
+(let (?e33 (bvxor ?e9 (sign_extend[4] ?e2)))
+(let (?e34 (ite (bvslt ?e17 v0) bv1[1] bv0[1]))
+(let (?e35 (extract[0:0] ?e23))
+(let (?e36 (sign_extend[9] ?e35))
+(let (?e37 (bvadd ?e9 (sign_extend[8] ?e27)))
+(let (?e38 (ite (= bv1[1] (extract[2:2] ?e36)) ?e14 (sign_extend[8] ?e7)))
+(let (?e39 (ite (bvult ?e30 ?e27) bv1[1] bv0[1]))
+(let (?e40 (bvsmod (sign_extend[7] ?e27) v0))
+(let (?e41 (ite (= ?e14 ?e9) bv1[1] bv0[1]))
+(let (?e42 (bvsmod (sign_extend[7] ?e7) ?e40))
+(let (?e43 (ite (= ?e41 ?e39) bv1[1] bv0[1]))
+(let (?e44 (bvudiv ?e25 ?e4))
+(let (?e45 (ite (bvsge ?e38 (zero_extend[1] ?e5)) bv1[1] bv0[1]))
+(let (?e46 (bvnor ?e14 (zero_extend[8] ?e29)))
+(let (?e47 (ite (= bv1[1] (extract[0:0] ?e22)) ?e36 (sign_extend[2] ?e6)))
+(let (?e48 (ite (bvslt ?e28 (sign_extend[7] ?e35)) bv1[1] bv0[1]))
+(let (?e49 (ite (= bv1[1] (extract[0:0] ?e18)) ?e36 (sign_extend[9] ?e35)))
+(let (?e50 (bvand ?e44 (sign_extend[1] ?e16)))
+(let (?e51 (ite (bvugt (sign_extend[7] ?e19) ?e3) bv1[1] bv0[1]))
+(let (?e52 (extract[0:0] ?e29))
+(let (?e53 (bvxor ?e35 ?e19))
+(let (?e54 (repeat[5] ?e24))
+(let (?e55 (bvor ?e4 (zero_extend[8] ?e24)))
+(let (?e56 (ite (bvult ?e36 (sign_extend[2] ?e10)) bv1[1] bv0[1]))
+(let (?e57 (bvlshr (zero_extend[12] ?e41) ?e21))
+(let (?e58 (bvnot ?e14))
+(let (?e59 (ite (bvsle ?e25 (zero_extend[1] ?e26)) bv1[1] bv0[1]))
+(let (?e60 (bvurem (zero_extend[8] ?e20) ?e4))
+(let (?e61 (concat ?e34 ?e38))
+(let (?e62 (bvneg ?e48))
+(let (?e63 (ite (bvuge ?e38 (zero_extend[1] ?e28)) bv1[1] bv0[1]))
+(let (?e64 (bvneg ?e46))
+(let (?e65 (repeat[12] ?e30))
+(let (?e66 (repeat[1] ?e36))
+(let (?e67 (bvor ?e28 (zero_extend[7] ?e24)))
+(let (?e68 (ite (bvsle (sign_extend[4] ?e24) ?e54) bv1[1] bv0[1]))
+(let (?e69 (ite (bvult (zero_extend[1] ?e67) ?e4) bv1[1] bv0[1]))
+(let (?e70 (ite (bvsgt ?e7 ?e62) bv1[1] bv0[1]))
+(let (?e71 (bvcomp ?e68 ?e19))
+(let (?e72 (bvor (sign_extend[8] ?e52) ?e58))
+(let (?e73 (sign_extend[1] ?e48))
+(let (?e74 (bvadd (zero_extend[7] ?e30) ?e5))
+(let (?e75 (ite (bvsle ?e47 (zero_extend[9] ?e59)) bv1[1] bv0[1]))
+(let (?e76 (bvnot ?e30))
+(let (?e77 (extract[0:0] ?e11))
+(let (?e78 (bvsdiv (zero_extend[7] ?e29) ?e3))
+(let (?e79 (bvurem (zero_extend[1] ?e74) ?e38))
+(let (?e80 (ite (bvslt ?e25 ?e4) bv1[1] bv0[1]))
+(let (?e81 (sign_extend[0] ?e43))
+(let (?e82 (bvadd ?e13 ?e26))
+(let (?e83 (bvnot ?e67))
+(let (?e84 (bvor ?e45 ?e22))
+(let (?e85 (bvsmod (sign_extend[7] ?e52) v0))
+(let (?e86 (bvadd (zero_extend[8] ?e19) ?e14))
+(let (?e87 (bvmul ?e44 ?e55))
+(let (?e88 (bvurem (zero_extend[7] ?e22) ?e32))
+(let (?e89 (bvand ?e85 (zero_extend[7] ?e84)))
+(let (?e90 (bvor ?e72 (sign_extend[8] ?e23)))
+(let (?e91 (bvor ?e6 (sign_extend[7] ?e19)))
+(let (?e92 (bvudiv (zero_extend[8] ?e23) ?e60))
+(let (?e93 (ite (bvslt ?e46 ?e44) bv1[1] bv0[1]))
+(let (?e94 (bvxnor (sign_extend[4] ?e74) ?e65))
+(let (?e95 (ite (bvugt ?e87 (sign_extend[8] ?e30)) bv1[1] bv0[1]))
+(let (?e96 (bvashr (zero_extend[1] ?e14) ?e47))
+(let (?e97 (rotate_left[3] ?e83))
+(let (?e98 (ite (bvult (zero_extend[3] ?e2) ?e3) bv1[1] bv0[1]))
+(let (?e99 (ite (bvslt (zero_extend[1] ?e90) ?e66) bv1[1] bv0[1]))
+(let (?e100 (ite (bvult (zero_extend[7] ?e23) ?e89) bv1[1] bv0[1]))
+(let (?e101 (rotate_right[0] ?e60))
+(let (?e102 (ite (bvslt (sign_extend[7] ?e62) ?e26) bv1[1] bv0[1]))
+(let (?e103 (ite (bvugt ?e65 (sign_extend[4] v0)) bv1[1] bv0[1]))
+(let (?e104 (bvnand ?e57 (sign_extend[12] ?e71)))
+(let (?e105 (bvnor v1 (zero_extend[13] ?e30)))
+(flet ($e106 (bvsge ?e75 ?e56))
+(flet ($e107 (bvsgt (sign_extend[8] ?e27) ?e25))
+(flet ($e108 (bvugt (zero_extend[8] ?e80) ?e15))
+(flet ($e109 (bvule (sign_extend[2] ?e89) ?e49))
+(flet ($e110 (bvsge ?e91 (zero_extend[7] ?e51)))
+(flet ($e111 (distinct ?e60 (sign_extend[8] ?e34)))
+(flet ($e112 (bvugt (sign_extend[7] ?e98) ?e74))
+(flet ($e113 (bvsgt ?e27 ?e45))
+(flet ($e114 (bvult (zero_extend[8] ?e70) ?e25))
+(flet ($e115 (bvsgt (sign_extend[6] ?e83) v1))
+(flet ($e116 (bvult (sign_extend[9] ?e20) ?e36))
+(flet ($e117 (bvsle (sign_extend[4] ?e25) ?e21))
+(flet ($e118 (bvuge ?e94 (zero_extend[3] ?e4)))
+(flet ($e119 (bvslt ?e93 ?e30))
+(flet ($e120 (bvsgt ?e77 ?e75))
+(flet ($e121 (bvsgt ?e31 (zero_extend[10] ?e18)))
+(flet ($e122 (bvult v1 (zero_extend[6] ?e91)))
+(flet ($e123 (bvugt (sign_extend[8] ?e43) ?e4))
+(flet ($e124 (bvsle ?e55 (sign_extend[8] ?e22)))
+(flet ($e125 (= (zero_extend[7] ?e34) ?e83))
+(flet ($e126 (bvsge (zero_extend[8] ?e52) ?e64))
+(flet ($e127 (bvslt v1 (zero_extend[6] ?e91)))
+(flet ($e128 (bvugt ?e60 ?e64))
+(flet ($e129 (bvsgt ?e85 (zero_extend[7] ?e27)))
+(flet ($e130 (bvsle (sign_extend[8] ?e63) ?e25))
+(flet ($e131 (bvuge ?e90 (zero_extend[1] ?e5)))
+(flet ($e132 (distinct (sign_extend[1] ?e88) ?e37))
+(flet ($e133 (bvsge (zero_extend[1] ?e78) ?e90))
+(flet ($e134 (bvsle ?e22 ?e45))
+(flet ($e135 (bvult ?e105 (zero_extend[4] ?e61)))
+(flet ($e136 (bvuge (sign_extend[4] ?e28) ?e94))
+(flet ($e137 (bvugt ?e4 (sign_extend[1] v0)))
+(flet ($e138 (bvslt ?e69 ?e100))
+(flet ($e139 (bvsle ?e72 ?e14))
+(flet ($e140 (distinct ?e82 ?e89))
+(flet ($e141 (bvsle (zero_extend[12] ?e29) ?e57))
+(flet ($e142 (bvsge (sign_extend[1] ?e60) ?e66))
+(flet ($e143 (bvslt ?e59 ?e95))
+(flet ($e144 (bvsle ?e25 ?e87))
+(flet ($e145 (bvslt ?e6 (sign_extend[7] ?e30)))
+(flet ($e146 (= (sign_extend[1] ?e10) ?e38))
+(flet ($e147 (bvult ?e47 (sign_extend[9] ?e7)))
+(flet ($e148 (bvugt ?e16 ?e3))
+(flet ($e149 (bvult (zero_extend[1] ?e78) ?e33))
+(flet ($e150 (bvuge ?e34 ?e48))
+(flet ($e151 (bvsge ?e91 (zero_extend[7] ?e100)))
+(flet ($e152 (bvugt (sign_extend[8] ?e62) ?e101))
+(flet ($e153 (bvsgt (zero_extend[8] ?e53) ?e50))
+(flet ($e154 (bvugt ?e87 (zero_extend[8] ?e84)))
+(flet ($e155 (bvule (zero_extend[3] ?e2) ?e74))
+(flet ($e156 (bvslt (zero_extend[4] ?e44) ?e104))
+(flet ($e157 (bvsgt (zero_extend[1] ?e51) ?e73))
+(flet ($e158 (bvuge ?e32 (sign_extend[7] ?e75)))
+(flet ($e159 (bvugt ?e33 ?e9))
+(flet ($e160 (bvslt (sign_extend[1] ?e78) ?e58))
+(flet ($e161 (bvsle (zero_extend[4] ?e61) ?e105))
+(flet ($e162 (bvsge ?e94 (zero_extend[3] ?e4)))
+(flet ($e163 (bvslt ?e98 ?e27))
+(flet ($e164 (bvslt ?e43 ?e95))
+(flet ($e165 (bvugt ?e81 ?e52))
+(flet ($e166 (bvsgt ?e96 (sign_extend[9] ?e56)))
+(flet ($e167 (bvugt ?e71 ?e27))
+(flet ($e168 (bvslt ?e23 ?e24))
+(flet ($e169 (bvslt ?e37 ?e92))
+(flet ($e170 (bvuge ?e58 ?e15))
+(flet ($e171 (bvsge (zero_extend[7] ?e30) ?e74))
+(flet ($e172 (= ?e29 ?e34))
+(flet ($e173 (bvsle (zero_extend[4] ?e52) ?e54))
+(flet ($e174 (bvult ?e36 (zero_extend[2] ?e3)))
+(flet ($e175 (= (zero_extend[5] ?e97) ?e57))
+(flet ($e176 (bvuge ?e14 (sign_extend[8] ?e95)))
+(flet ($e177 (bvult (zero_extend[7] ?e70) ?e17))
+(flet ($e178 (bvslt ?e50 (sign_extend[8] ?e75)))
+(flet ($e179 (bvuge (zero_extend[7] ?e51) ?e91))
+(flet ($e180 (bvugt (sign_extend[4] ?e54) ?e64))
+(flet ($e181 (bvule (zero_extend[4] ?e78) ?e65))
+(flet ($e182 (= (sign_extend[8] ?e51) ?e25))
+(flet ($e183 (bvsgt ?e75 ?e68))
+(flet ($e184 (distinct (sign_extend[8] ?e45) ?e55))
+(flet ($e185 (bvugt ?e31 (sign_extend[2] ?e92)))
+(flet ($e186 (bvsgt (zero_extend[7] ?e20) ?e8))
+(flet ($e187 (= ?e49 (zero_extend[9] ?e77)))
+(flet ($e188 (bvsgt ?e32 ?e97))
+(flet ($e189 (bvsgt ?e14 ?e50))
+(flet ($e190 (bvuge (zero_extend[7] ?e43) ?e26))
+(flet ($e191 (bvslt (zero_extend[8] ?e103) ?e50))
+(flet ($e192 (bvsle ?e92 (sign_extend[8] ?e27)))
+(flet ($e193 (bvsle ?e58 ?e9))
+(flet ($e194 (bvuge (zero_extend[7] ?e27) ?e82))
+(flet ($e195 (bvule ?e14 (zero_extend[8] ?e84)))
+(flet ($e196 (= ?e55 ?e58))
+(flet ($e197 (bvslt ?e104 (sign_extend[12] ?e99)))
+(flet ($e198 (bvule ?e64 ?e33))
+(flet ($e199 (bvult ?e10 ?e32))
+(flet ($e200 (bvule (sign_extend[7] ?e43) ?e74))
+(flet ($e201 (bvslt ?e58 (zero_extend[8] ?e43)))
+(flet ($e202 (= ?e46 ?e60))
+(flet ($e203 (= ?e54 (zero_extend[4] ?e23)))
+(flet ($e204 (bvsgt ?e38 (zero_extend[1] ?e42)))
+(flet ($e205 (distinct ?e72 (zero_extend[1] ?e97)))
+(flet ($e206 (bvult (zero_extend[7] ?e11) ?e83))
+(flet ($e207 (bvuge ?e27 ?e52))
+(flet ($e208 (bvsge ?e36 (sign_extend[9] ?e45)))
+(flet ($e209 (bvsge (zero_extend[7] ?e81) ?e91))
+(flet ($e210 (bvult ?e33 ?e14))
+(flet ($e211 (bvslt ?e64 (zero_extend[1] ?e42)))
+(flet ($e212 (bvult (zero_extend[7] ?e75) ?e6))
+(flet ($e213 (= v0 ?e97))
+(flet ($e214 (bvsgt ?e48 ?e27))
+(flet ($e215 (= ?e77 ?e43))
+(flet ($e216 (bvuge ?e43 ?e45))
+(flet ($e217 (bvule ?e10 ?e40))
+(flet ($e218 (bvsle (zero_extend[2] ?e6) ?e47))
+(flet ($e219 (distinct (zero_extend[1] ?e17) ?e14))
+(flet ($e220 (bvsge ?e45 ?e84))
+(flet ($e221 (bvsle (sign_extend[4] ?e11) ?e54))
+(flet ($e222 (bvult ?e71 ?e69))
+(flet ($e223 (= ?e16 (sign_extend[7] ?e34)))
+(flet ($e224 (bvsle (sign_extend[8] ?e93) ?e55))
+(flet ($e225 (bvult ?e42 ?e8))
+(flet ($e226 (bvsle ?e104 (zero_extend[4] ?e50)))
+(flet ($e227 (bvult ?e42 (zero_extend[7] ?e76)))
+(flet ($e228 (bvsle ?e25 (sign_extend[8] ?e20)))
+(flet ($e229 (= (sign_extend[10] ?e71) ?e31))
+(flet ($e230 (bvsge (sign_extend[1] ?e6) ?e50))
+(flet ($e231 (bvsgt (zero_extend[7] ?e93) ?e83))
+(flet ($e232 (bvugt ?e98 ?e18))
+(flet ($e233 (bvsge ?e26 (sign_extend[7] ?e23)))
+(flet ($e234 (bvsgt v1 (sign_extend[13] ?e76)))
+(flet ($e235 (bvugt ?e2 (sign_extend[4] ?e24)))
+(flet ($e236 (bvslt ?e61 (zero_extend[1] ?e9)))
+(flet ($e237 (= ?e10 ?e16))
+(flet ($e238 (= ?e91 (zero_extend[7] ?e100)))
+(flet ($e239 (bvsgt (zero_extend[6] ?e73) ?e3))
+(flet ($e240 (bvuge ?e71 ?e30))
+(flet ($e241 (bvsgt ?e104 (zero_extend[4] ?e92)))
+(flet ($e242 (bvsle ?e41 ?e70))
+(flet ($e243 (distinct (zero_extend[5] ?e46) v1))
+(flet ($e244 (= ?e79 (zero_extend[8] ?e99)))
+(flet ($e245 (bvuge ?e99 ?e99))
+(flet ($e246 (bvslt ?e56 ?e18))
+(flet ($e247 (bvslt (zero_extend[7] ?e95) ?e88))
+(flet ($e248 (bvugt ?e31 (zero_extend[10] ?e71)))
+(flet ($e249 (bvsgt (sign_extend[13] ?e45) v1))
+(flet ($e250 (bvsle ?e96 (sign_extend[2] ?e88)))
+(flet ($e251 (distinct (zero_extend[6] ?e3) ?e105))
+(flet ($e252 (bvugt ?e36 (zero_extend[1] ?e101)))
+(flet ($e253 (bvule ?e97 ?e82))
+(flet ($e254 (bvugt ?e61 (sign_extend[9] ?e56)))
+(flet ($e255 (bvsgt (sign_extend[7] ?e63) ?e89))
+(flet ($e256 (bvsgt (zero_extend[7] ?e103) ?e88))
+(flet ($e257 (bvslt ?e21 (sign_extend[12] ?e59)))
+(flet ($e258 (bvsle (sign_extend[4] ?e59) ?e54))
+(flet ($e259 (distinct ?e84 ?e100))
+(flet ($e260 (bvule (zero_extend[12] ?e99) ?e21))
+(flet ($e261 (= ?e23 ?e51))
+(flet ($e262 (= ?e43 ?e56))
+(flet ($e263 (= ?e81 ?e45))
+(flet ($e264 (bvslt (sign_extend[1] ?e87) ?e66))
+(flet ($e265 (bvult ?e27 ?e77))
+(flet ($e266 (bvsle (zero_extend[12] ?e52) ?e57))
+(flet ($e267 (bvuge (sign_extend[8] ?e99) ?e86))
+(flet ($e268 (bvule (sign_extend[4] ?e51) ?e2))
+(flet ($e269 (bvsle (sign_extend[8] ?e12) ?e92))
+(flet ($e270 (distinct ?e104 (zero_extend[12] ?e20)))
+(flet ($e271 (= ?e9 (sign_extend[8] ?e102)))
+(flet ($e272 (bvult (zero_extend[8] ?e39) ?e86))
+(flet ($e273 (bvuge (sign_extend[7] ?e51) v0))
+(flet ($e274 (bvult (zero_extend[9] ?e24) ?e96))
+(flet ($e275 (= ?e65 (zero_extend[4] ?e82)))
+(flet ($e276 (bvsge ?e50 (sign_extend[8] ?e59)))
+(flet ($e277 (bvsge (zero_extend[8] ?e29) ?e38))
+(flet ($e278 (bvsle (sign_extend[1] ?e42) ?e25))
+(flet ($e279 (bvuge ?e86 (zero_extend[8] ?e48)))
+(flet ($e280 (= ?e36 (sign_extend[1] ?e38)))
+(flet ($e281 (= (sign_extend[8] ?e59) ?e9))
+(flet ($e282 (bvule ?e14 (sign_extend[8] ?e43)))
+(flet ($e283 (bvslt (sign_extend[7] ?e63) v0))
+(flet ($e284 (bvslt ?e43 ?e29))
+(flet ($e285 (bvuge (sign_extend[2] ?e4) ?e31))
+(flet ($e286 (bvsle ?e49 ?e61))
+(flet ($e287 (bvult (zero_extend[3] ?e2) ?e13))
+(flet ($e288 (distinct ?e14 (zero_extend[8] ?e24)))
+(flet ($e289 (bvsgt (sign_extend[8] ?e76) ?e4))
+(flet ($e290 (bvult ?e53 ?e7))
+(flet ($e291 (bvuge ?e103 ?e69))
+(flet ($e292 (bvugt ?e5 (sign_extend[7] ?e29)))
+(flet ($e293 (distinct ?e79 (zero_extend[1] ?e32)))
+(flet ($e294 (bvslt (zero_extend[3] ?e54) ?e17))
+(flet ($e295 (bvslt (sign_extend[11] ?e20) ?e94))
+(flet ($e296 (bvugt ?e64 (sign_extend[1] ?e16)))
+(flet ($e297 (bvsgt ?e50 (zero_extend[8] ?e63)))
+(flet ($e298 (bvslt ?e89 (sign_extend[7] ?e23)))
+(flet ($e299 (bvslt ?e74 (sign_extend[7] ?e30)))
+(flet ($e300 (bvult (zero_extend[2] ?e74) ?e66))
+(flet ($e301 (bvsle ?e2 (zero_extend[4] ?e35)))
+(flet ($e302 (bvsge ?e48 ?e23))
+(flet ($e303 (= ?e31 (zero_extend[10] ?e68)))
+(flet ($e304 (= ?e16 (sign_extend[7] ?e24)))
+(flet ($e305 (= ?e47 (zero_extend[1] ?e60)))
+(flet ($e306 (distinct (sign_extend[1] ?e40) ?e25))
+(flet ($e307 (bvult (zero_extend[1] ?e42) ?e101))
+(flet ($e308 (bvuge ?e61 (sign_extend[1] ?e86)))
+(flet ($e309 (bvuge ?e31 (sign_extend[10] ?e22)))
+(flet ($e310 (bvult (zero_extend[12] ?e69) ?e104))
+(flet ($e311 (bvugt ?e74 (sign_extend[7] ?e48)))
+(flet ($e312 (bvslt ?e5 ?e16))
+(flet ($e313 (bvule ?e64 (zero_extend[8] ?e98)))
+(flet ($e314 (bvsle ?e59 ?e51))
+(flet ($e315 (= (sign_extend[8] ?e30) ?e90))
+(flet ($e316 (bvuge ?e57 (sign_extend[8] ?e2)))
+(flet ($e317 (bvsgt ?e78 ?e16))
+(flet ($e318 (bvult ?e80 ?e22))
+(flet ($e319 (distinct ?e4 (zero_extend[1] ?e28)))
+(flet ($e320 (bvuge (sign_extend[7] ?e84) ?e42))
+(flet ($e321 (bvult ?e43 ?e52))
+(flet ($e322 (bvule (sign_extend[7] ?e102) ?e88))
+(flet ($e323 (distinct ?e78 ?e5))
+(flet ($e324 (bvugt (zero_extend[7] ?e48) ?e85))
+(flet ($e325 (bvslt (zero_extend[7] ?e102) ?e10))
+(flet ($e326 (bvule ?e83 (sign_extend[3] ?e54)))
+(flet ($e327 (bvsge (sign_extend[5] ?e13) ?e57))
+(flet ($e328 (bvult (sign_extend[3] ?e25) ?e65))
+(flet ($e329 (bvugt (zero_extend[1] ?e66) ?e31))
+(flet ($e330 (= (sign_extend[1] ?e89) ?e46))
+(flet ($e331 (distinct ?e58 ?e15))
+(flet ($e332 (bvule ?e99 ?e43))
+(flet ($e333 (distinct ?e59 ?e80))
+(flet ($e334 (bvsle (zero_extend[9] ?e95) ?e47))
+(flet ($e335 (bvsle ?e91 ?e32))
+(flet ($e336 (bvuge (zero_extend[13] ?e76) ?e105))
+(flet ($e337 (bvule (zero_extend[8] ?e71) ?e86))
+(flet ($e338 (distinct ?e89 ?e42))
+(flet ($e339 (bvule (zero_extend[2] ?e13) ?e47))
+(flet ($e340 (distinct ?e10 ?e5))
+(flet ($e341 (bvule (sign_extend[7] ?e100) ?e5))
+(flet ($e342 (bvugt (sign_extend[8] ?e54) ?e21))
+(flet ($e343 (bvult ?e8 (sign_extend[7] ?e76)))
+(flet ($e344 (bvuge (sign_extend[7] ?e59) ?e10))
+(flet ($e345 (distinct (zero_extend[8] ?e53) ?e38))
+(flet ($e346 (bvsge ?e104 (zero_extend[12] ?e68)))
+(flet ($e347 (bvult (sign_extend[9] ?e12) ?e66))
+(flet ($e348 (bvugt (sign_extend[7] ?e19) ?e91))
+(flet ($e349 (bvsle ?e76 ?e34))
+(flet ($e350 (bvsle ?e46 (sign_extend[8] ?e30)))
+(flet ($e351 (= (zero_extend[11] ?e41) ?e65))
+(flet ($e352 (bvugt ?e32 ?e83))
+(flet ($e353 (bvuge ?e70 ?e76))
+(flet ($e354 (bvugt ?e37 (zero_extend[8] ?e81)))
+(flet ($e355 (bvult (zero_extend[8] ?e53) ?e55))
+(flet ($e356 (bvule (zero_extend[9] ?e7) ?e47))
+(flet ($e357 (bvsle (zero_extend[9] ?e99) ?e36))
+(flet ($e358 (bvule (sign_extend[7] ?e98) ?e16))
+(flet ($e359 (bvslt ?e60 (zero_extend[8] ?e71)))
+(flet ($e360 (bvult (zero_extend[7] ?e54) ?e94))
+(flet ($e361 (bvule (zero_extend[2] ?e37) ?e31))
+(flet ($e362 (bvule (sign_extend[13] ?e48) ?e105))
+(flet ($e363 (bvsgt (zero_extend[8] ?e23) ?e14))
+(flet ($e364 (bvult ?e94 (zero_extend[3] ?e60)))
+(flet ($e365 (bvult (zero_extend[1] ?e78) ?e15))
+(flet ($e366 (bvsgt ?e48 ?e62))
+(flet ($e367 (bvult ?e77 ?e77))
+(flet ($e368 (bvsle (zero_extend[11] ?e34) ?e65))
+(flet ($e369 (distinct ?e15 (sign_extend[8] ?e71)))
+(flet ($e370 (bvugt ?e84 ?e27))
+(flet ($e371 (bvslt ?e25 ?e25))
+(flet ($e372 (bvult ?e16 ?e78))
+(flet ($e373 (bvugt (sign_extend[8] ?e19) ?e38))
+(flet ($e374 (bvugt ?e50 (sign_extend[8] ?e18)))
+(flet ($e375 (bvule ?e95 ?e76))
+(flet ($e376 (bvsle (zero_extend[7] ?e23) ?e85))
+(flet ($e377 (bvsge ?e12 ?e95))
+(flet ($e378 (bvule ?e55 ?e101))
+(flet ($e379 (bvsge ?e37 (zero_extend[1] ?e97)))
+(flet ($e380 (bvugt ?e31 (zero_extend[2] ?e50)))
+(flet ($e381 (bvsge ?e36 (sign_extend[2] ?e42)))
+(flet ($e382 (bvule ?e101 (zero_extend[8] ?e84)))
+(flet ($e383 (bvsgt (sign_extend[1] ?e28) ?e64))
+(flet ($e384 (bvugt ?e30 ?e34))
+(flet ($e385 (bvsle ?e104 (zero_extend[4] ?e60)))
+(flet ($e386 (bvslt ?e74 ?e6))
+(flet ($e387 (bvsle ?e18 ?e52))
+(flet ($e388 (bvuge ?e102 ?e48))
+(flet ($e389 (bvuge ?e69 ?e27))
+(flet ($e390 (distinct ?e50 ?e79))
+(flet ($e391 (bvule ?e48 ?e98))
+(flet ($e392 (bvsge (sign_extend[1] ?e94) ?e104))
+(flet ($e393 (bvsge ?e67 (sign_extend[3] ?e54)))
+(flet ($e394 (and $e172 $e310))
+(flet ($e395 (if_then_else $e280 $e364 $e221))
+(flet ($e396 (and $e217 $e330))
+(flet ($e397 (and $e208 $e286))
+(flet ($e398 (not $e354))
+(flet ($e399 (iff $e253 $e164))
+(flet ($e400 (or $e240 $e347))
+(flet ($e401 (if_then_else $e112 $e365 $e106))
+(flet ($e402 (not $e212))
+(flet ($e403 (iff $e207 $e129))
+(flet ($e404 (or $e386 $e363))
+(flet ($e405 (not $e117))
+(flet ($e406 (xor $e274 $e322))
+(flet ($e407 (xor $e285 $e132))
+(flet ($e408 (iff $e333 $e367))
+(flet ($e409 (and $e406 $e317))
+(flet ($e410 (xor $e144 $e169))
+(flet ($e411 (if_then_else $e381 $e407 $e410))
+(flet ($e412 (xor $e376 $e269))
+(flet ($e413 (xor $e315 $e187))
+(flet ($e414 (implies $e378 $e252))
+(flet ($e415 (xor $e264 $e275))
+(flet ($e416 (implies $e281 $e138))
+(flet ($e417 (implies $e412 $e256))
+(flet ($e418 (iff $e248 $e351))
+(flet ($e419 (xor $e124 $e304))
+(flet ($e420 (or $e368 $e358))
+(flet ($e421 (implies $e382 $e196))
+(flet ($e422 (iff $e337 $e415))
+(flet ($e423 (not $e203))
+(flet ($e424 (implies $e150 $e308))
+(flet ($e425 (and $e329 $e241))
+(flet ($e426 (xor $e268 $e314))
+(flet ($e427 (xor $e373 $e189))
+(flet ($e428 (or $e171 $e193))
+(flet ($e429 (and $e125 $e262))
+(flet ($e430 (or $e271 $e140))
+(flet ($e431 (if_then_else $e390 $e287 $e215))
+(flet ($e432 (implies $e416 $e332))
+(flet ($e433 (xor $e279 $e295))
+(flet ($e434 (not $e301))
+(flet ($e435 (if_then_else $e239 $e270 $e195))
+(flet ($e436 (not $e224))
+(flet ($e437 (if_then_else $e258 $e395 $e309))
+(flet ($e438 (if_then_else $e267 $e265 $e356))
+(flet ($e439 (if_then_else $e403 $e223 $e331))
+(flet ($e440 (xor $e123 $e186))
+(flet ($e441 (not $e213))
+(flet ($e442 (xor $e128 $e361))
+(flet ($e443 (xor $e319 $e170))
+(flet ($e444 (if_then_else $e355 $e425 $e398))
+(flet ($e445 (if_then_else $e436 $e379 $e218))
+(flet ($e446 (or $e131 $e109))
+(flet ($e447 (implies $e166 $e357))
+(flet ($e448 (iff $e211 $e377))
+(flet ($e449 (implies $e228 $e151))
+(flet ($e450 (if_then_else $e143 $e338 $e318))
+(flet ($e451 (not $e234))
+(flet ($e452 (xor $e444 $e383))
+(flet ($e453 (implies $e229 $e296))
+(flet ($e454 (implies $e311 $e107))
+(flet ($e455 (and $e237 $e182))
+(flet ($e456 (iff $e210 $e435))
+(flet ($e457 (if_then_else $e353 $e111 $e292))
+(flet ($e458 (not $e108))
+(flet ($e459 (xor $e148 $e113))
+(flet ($e460 (xor $e273 $e163))
+(flet ($e461 (if_then_else $e305 $e393 $e277))
+(flet ($e462 (xor $e335 $e156))
+(flet ($e463 (not $e437))
+(flet ($e464 (iff $e246 $e321))
+(flet ($e465 (and $e442 $e352))
+(flet ($e466 (iff $e326 $e255))
+(flet ($e467 (xor $e257 $e439))
+(flet ($e468 (implies $e266 $e130))
+(flet ($e469 (xor $e115 $e328))
+(flet ($e470 (implies $e190 $e293))
+(flet ($e471 (implies $e411 $e350))
+(flet ($e472 (implies $e197 $e174))
+(flet ($e473 (not $e325))
+(flet ($e474 (or $e454 $e251))
+(flet ($e475 (and $e162 $e206))
+(flet ($e476 (implies $e201 $e242))
+(flet ($e477 (not $e346))
+(flet ($e478 (xor $e216 $e245))
+(flet ($e479 (not $e230))
+(flet ($e480 (xor $e137 $e152))
+(flet ($e481 (not $e205))
+(flet ($e482 (if_then_else $e283 $e443 $e343))
+(flet ($e483 (xor $e461 $e431))
+(flet ($e484 (if_then_else $e342 $e387 $e455))
+(flet ($e485 (not $e199))
+(flet ($e486 (if_then_else $e290 $e178 $e465))
+(flet ($e487 (xor $e327 $e448))
+(flet ($e488 (if_then_else $e284 $e235 $e486))
+(flet ($e489 (not $e488))
+(flet ($e490 (xor $e344 $e282))
+(flet ($e491 (or $e183 $e147))
+(flet ($e492 (and $e380 $e402))
+(flet ($e493 (implies $e119 $e244))
+(flet ($e494 (or $e476 $e263))
+(flet ($e495 (if_then_else $e298 $e249 $e220))
+(flet ($e496 (if_then_else $e421 $e200 $e483))
+(flet ($e497 (implies $e493 $e388))
+(flet ($e498 (implies $e198 $e392))
+(flet ($e499 (if_then_else $e192 $e458 $e222))
+(flet ($e500 (xor $e467 $e288))
+(flet ($e501 (implies $e259 $e276))
+(flet ($e502 (or $e340 $e133))
+(flet ($e503 (if_then_else $e400 $e191 $e261))
+(flet ($e504 (if_then_else $e445 $e122 $e371))
+(flet ($e505 (iff $e394 $e175))
+(flet ($e506 (or $e360 $e468))
+(flet ($e507 (iff $e300 $e482))
+(flet ($e508 (implies $e194 $e324))
+(flet ($e509 (xor $e345 $e278))
+(flet ($e510 (implies $e504 $e341))
+(flet ($e511 (if_then_else $e466 $e441 $e334))
+(flet ($e512 (implies $e457 $e160))
+(flet ($e513 (implies $e302 $e135))
+(flet ($e514 (and $e158 $e227))
+(flet ($e515 (or $e479 $e238))
+(flet ($e516 (xor $e507 $e423))
+(flet ($e517 (if_then_else $e511 $e209 $e307))
+(flet ($e518 (if_then_else $e316 $e161 $e508))
+(flet ($e519 (and $e139 $e219))
+(flet ($e520 (implies $e434 $e472))
+(flet ($e521 (and $e477 $e470))
+(flet ($e522 (or $e481 $e498))
+(flet ($e523 (iff $e366 $e136))
+(flet ($e524 (and $e231 $e491))
+(flet ($e525 (xor $e475 $e179))
+(flet ($e526 (iff $e471 $e506))
+(flet ($e527 (and $e121 $e397))
+(flet ($e528 (and $e184 $e414))
+(flet ($e529 (and $e204 $e512))
+(flet ($e530 (if_then_else $e496 $e484 $e294))
+(flet ($e531 (if_then_else $e469 $e180 $e359))
+(flet ($e532 (not $e374))
+(flet ($e533 (not $e168))
+(flet ($e534 (xor $e451 $e396))
+(flet ($e535 (not $e430))
+(flet ($e536 (xor $e289 $e463))
+(flet ($e537 (xor $e522 $e424))
+(flet ($e538 (iff $e526 $e114))
+(flet ($e539 (if_then_else $e312 $e299 $e480))
+(flet ($e540 (xor $e523 $e533))
+(flet ($e541 (or $e422 $e531))
+(flet ($e542 (and $e370 $e202))
+(flet ($e543 (or $e515 $e226))
+(flet ($e544 (or $e489 $e127))
+(flet ($e545 (and $e188 $e516))
+(flet ($e546 (xor $e173 $e545))
+(flet ($e547 (if_then_else $e401 $e369 $e487))
+(flet ($e548 (and $e155 $e247))
+(flet ($e549 (and $e349 $e126))
+(flet ($e550 (or $e134 $e485))
+(flet ($e551 (if_then_else $e513 $e372 $e549))
+(flet ($e552 (xor $e417 $e521))
+(flet ($e553 (implies $e232 $e548))
+(flet ($e554 (not $e254))
+(flet ($e555 (if_then_else $e535 $e460 $e362))
+(flet ($e556 (or $e320 $e551))
+(flet ($e557 (if_then_else $e428 $e500 $e547))
+(flet ($e558 (not $e450))
+(flet ($e559 (iff $e503 $e236))
+(flet ($e560 (if_then_else $e142 $e250 $e146))
+(flet ($e561 (implies $e272 $e243))
+(flet ($e562 (implies $e552 $e185))
+(flet ($e563 (or $e440 $e141))
+(flet ($e564 (implies $e538 $e447))
+(flet ($e565 (iff $e404 $e456))
+(flet ($e566 (xor $e291 $e492))
+(flet ($e567 (iff $e167 $e348))
+(flet ($e568 (xor $e176 $e427))
+(flet ($e569 (if_then_else $e539 $e490 $e306))
+(flet ($e570 (implies $e339 $e563))
+(flet ($e571 (implies $e177 $e153))
+(flet ($e572 (if_then_else $e157 $e145 $e408))
+(flet ($e573 (iff $e473 $e399))
+(flet ($e574 (iff $e569 $e181))
+(flet ($e575 (and $e527 $e154))
+(flet ($e576 (or $e116 $e570))
+(flet ($e577 (and $e546 $e409))
+(flet ($e578 (xor $e225 $e566))
+(flet ($e579 (if_then_else $e446 $e561 $e525))
+(flet ($e580 (implies $e494 $e149))
+(flet ($e581 (if_then_else $e432 $e418 $e517))
+(flet ($e582 (if_then_else $e313 $e557 $e453))
+(flet ($e583 (implies $e464 $e581))
+(flet ($e584 (not $e560))
+(flet ($e585 (iff $e576 $e385))
+(flet ($e586 (xor $e575 $e420))
+(flet ($e587 (not $e564))
+(flet ($e588 (implies $e462 $e118))
+(flet ($e589 (xor $e474 $e571))
+(flet ($e590 (iff $e413 $e536))
+(flet ($e591 (or $e514 $e384))
+(flet ($e592 (and $e495 $e297))
+(flet ($e593 (xor $e165 $e505))
+(flet ($e594 (or $e562 $e565))
+(flet ($e595 (iff $e590 $e580))
+(flet ($e596 (and $e120 $e214))
+(flet ($e597 (iff $e583 $e540))
+(flet ($e598 (iff $e553 $e519))
+(flet ($e599 (and $e497 $e449))
+(flet ($e600 (if_then_else $e544 $e578 $e542))
+(flet ($e601 (and $e391 $e532))
+(flet ($e602 (not $e509))
+(flet ($e603 (or $e429 $e530))
+(flet ($e604 (implies $e336 $e528))
+(flet ($e605 (not $e600))
+(flet ($e606 (implies $e520 $e585))
+(flet ($e607 (if_then_else $e597 $e459 $e419))
+(flet ($e608 (xor $e524 $e594))
+(flet ($e609 (xor $e586 $e601))
+(flet ($e610 (and $e554 $e550))
+(flet ($e611 (or $e433 $e438))
+(flet ($e612 (xor $e591 $e502))
+(flet ($e613 (implies $e375 $e541))
+(flet ($e614 (xor $e584 $e605))
+(flet ($e615 (xor $e110 $e510))
+(flet ($e616 (xor $e567 $e587))
+(flet ($e617 (xor $e426 $e452))
+(flet ($e618 (implies $e518 $e499))
+(flet ($e619 (and $e610 $e589))
+(flet ($e620 (iff $e619 $e613))
+(flet ($e621 (xor $e555 $e233))
+(flet ($e622 (and $e593 $e611))
+(flet ($e623 (iff $e260 $e596))
+(flet ($e624 (iff $e582 $e323))
+(flet ($e625 (not $e534))
+(flet ($e626 (and $e603 $e598))
+(flet ($e627 (not $e624))
+(flet ($e628 (xor $e614 $e607))
+(flet ($e629 (xor $e501 $e595))
+(flet ($e630 (if_then_else $e478 $e617 $e478))
+(flet ($e631 (if_then_else $e604 $e612 $e303))
+(flet ($e632 (implies $e606 $e609))
+(flet ($e633 (iff $e572 $e615))
+(flet ($e634 (not $e558))
+(flet ($e635 (if_then_else $e559 $e592 $e628))
+(flet ($e636 (or $e577 $e631))
+(flet ($e637 (not $e573))
+(flet ($e638 (not $e623))
+(flet ($e639 (not $e405))
+(flet ($e640 (not $e625))
+(flet ($e641 (not $e630))
+(flet ($e642 (iff $e159 $e629))
+(flet ($e643 (iff $e627 $e621))
+(flet ($e644 (not $e637))
+(flet ($e645 (xor $e537 $e636))
+(flet ($e646 (or $e588 $e543))
+(flet ($e647 (and $e633 $e574))
+(flet ($e648 (xor $e632 $e641))
+(flet ($e649 (implies $e602 $e618))
+(flet ($e650 (implies $e389 $e640))
+(flet ($e651 (and $e642 $e643))
+(flet ($e652 (if_then_else $e651 $e608 $e620))
+(flet ($e653 (xor $e652 $e529))
+(flet ($e654 (xor $e622 $e646))
+(flet ($e655 (or $e648 $e650))
+(flet ($e656 (implies $e599 $e644))
+(flet ($e657 (and $e556 $e655))
+(flet ($e658 (iff $e634 $e647))
+(flet ($e659 (iff $e639 $e568))
+(flet ($e660 (xor $e657 $e616))
+(flet ($e661 (or $e638 $e579))
+(flet ($e662 (and $e660 $e661))
+(flet ($e663 (and $e658 $e645))
+(flet ($e664 (iff $e649 $e663))
+(flet ($e665 (not $e626))
+(flet ($e666 (and $e664 $e656))
+(flet ($e667 (xor $e654 $e662))
+(flet ($e668 (implies $e653 $e653))
+(flet ($e669 (if_then_else $e667 $e667 $e666))
+(flet ($e670 (or $e668 $e659))
+(flet ($e671 (implies $e670 $e665))
+(flet ($e672 (not $e669))
+(flet ($e673 (iff $e671 $e672))
+(flet ($e674 (or $e635 $e673))
+(flet ($e675 (and $e674 (not (= ?e9 bv0[9]))))
+(flet ($e676 (and $e675 (not (= ?e9 (bvnot bv0[9])))))
+(flet ($e677 (and $e676 (not (= ?e17 bv0[8]))))
+(flet ($e678 (and $e677 (not (= ?e17 (bvnot bv0[8])))))
+(flet ($e679 (and $e678 (not (= ?e40 bv0[8]))))
+(flet ($e680 (and $e679 (not (= ?e40 (bvnot bv0[8])))))
+(flet ($e681 (and $e680 (not (= ?e6 bv0[8]))))
+(flet ($e682 (and $e681 (not (= ?e4 bv0[9]))))
+(flet ($e683 (and $e682 (not (= v0 bv0[8]))))
+(flet ($e684 (and $e683 (not (= v0 (bvnot bv0[8])))))
+(flet ($e685 (and $e684 (not (= ?e32 bv0[8]))))
+(flet ($e686 (and $e685 (not (= ?e38 bv0[9]))))
+(flet ($e687 (and $e686 (not (= ?e60 bv0[9]))))
+(flet ($e688 (and $e687 (not (= ?e3 bv0[8]))))
+(flet ($e689 (and $e688 (not (= ?e3 (bvnot bv0[8])))))
+(flet ($e690 (and $e689 (not (= ?e10 bv0[8]))))
+(flet ($e691 (and $e690 (not (= ?e10 (bvnot bv0[8])))))
+$e691
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
-- 
2.30.2