From ea1bf0f7b4ecf3caa4acde82739fe87dc8543ad4 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 23 May 2009 14:26:17 +0000 Subject: [PATCH] Removing the "broken" directory. The contents of this directory have already been moved to /stp-tests/smt-problems git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@79 e59a4935-1847-0410-ae03-e826735625c1 --- broken/BROKEN | 5 - broken/fixed/little.smt | 22 -- broken/nextpoweroftwo064.smt | 628 ----------------------------------- 3 files changed, 655 deletions(-) delete mode 100644 broken/BROKEN delete mode 100644 broken/fixed/little.smt delete mode 100644 broken/nextpoweroftwo064.smt diff --git a/broken/BROKEN b/broken/BROKEN deleted file mode 100644 index be31678..0000000 --- a/broken/BROKEN +++ /dev/null @@ -1,5 +0,0 @@ -nextpoweroftwo064.smt ---- -With optimizations disabled it finishes in 7.3 seconds (on my machine). With optimizations enabled it uses up all the available virtual memory (atleast twice more than when optimizations are disabled). - - diff --git a/broken/fixed/little.smt b/broken/fixed/little.smt deleted file mode 100644 index a87e621..0000000 --- a/broken/fixed/little.smt +++ /dev/null @@ -1,22 +0,0 @@ -( -benchmark temp20.smt -:source {Minkeyrink Solver} -:status unsat -:difficulty {1} -:category {crafted} -:logic QF_BV -:extrafuns ((sym1 BitVec[1])) -:extrafuns ((sym2 BitVec[1])) -:extrafuns ((sym3 BitVec[1])) - - -; Off-by-one in the bvlshr was causing the problem. Fixed in #54 - -:assumption (= (bvlshr sym1 sym2) sym3) -:assumption (= (bvlshr sym3 sym2) sym1) -:assumption (not (= sym2 bv0[1])) -:assumption (not (= sym1 bv0[1])) - - -) - diff --git a/broken/nextpoweroftwo064.smt b/broken/nextpoweroftwo064.smt deleted file mode 100644 index 977a945..0000000 --- a/broken/nextpoweroftwo064.smt +++ /dev/null @@ -1,628 +0,0 @@ -(benchmark nextpoweroftwo064.smt -:source { -We verify the correctness of the "next power of 2 algorithm" -from the book "hacker's delight" (Warren Jr., Henry). - -Algorithm: -int next_power_of_2 (int x) -\{ - int i; - x--; - for (i = 1; i < sizeof(int) * 8; i = i * 2) - x = x | (x >> i) - return x + 1; -\} - -Bit-width: 64 - -Contributed by Robert Brummayer (robert.brummayer@gmail.com). -} -:status unsat -:category { crafted } -:logic QF_BV -:difficulty { 5 } -:extrafuns ((x BitVec[64])) -:formula -(let (?e1 bv1[64]) -(let (?e2 bv2[64]) -(let (?e3 bv4[64]) -(let (?e4 bv8[64]) -(let (?e5 bv16[64]) -(let (?e6 bv32[64]) -(let (?e7 bv64[64]) -(let (?e8 bv128[64]) -(let (?e9 bv256[64]) -(let (?e10 bv512[64]) -(let (?e11 bv1024[64]) -(let (?e12 bv2048[64]) -(let (?e13 bv4096[64]) -(let (?e14 bv8192[64]) -(let (?e15 bv16384[64]) -(let (?e16 bv32768[64]) -(let (?e17 bv65536[64]) -(let (?e18 bv131072[64]) -(let (?e19 bv262144[64]) -(let (?e20 bv524288[64]) -(let (?e21 bv1048576[64]) -(let (?e22 bv2097152[64]) -(let (?e23 bv4194304[64]) -(let (?e24 bv8388608[64]) -(let (?e25 bv16777216[64]) -(let (?e26 bv33554432[64]) -(let (?e27 bv67108864[64]) -(let (?e28 bv134217728[64]) -(let (?e29 bv268435456[64]) -(let (?e30 bv536870912[64]) -(let (?e31 bv1073741824[64]) -(let (?e32 bv2147483648[64]) -(let (?e33 bv4294967296[64]) -(let (?e34 bv8589934592[64]) -(let (?e35 bv17179869184[64]) -(let (?e36 bv34359738368[64]) -(let (?e37 bv68719476736[64]) -(let (?e38 bv137438953472[64]) -(let (?e39 bv274877906944[64]) -(let (?e40 bv549755813888[64]) -(let (?e41 bv1099511627776[64]) -(let (?e42 bv2199023255552[64]) -(let (?e43 bv4398046511104[64]) -(let (?e44 bv8796093022208[64]) -(let (?e45 bv17592186044416[64]) -(let (?e46 bv35184372088832[64]) -(let (?e47 bv70368744177664[64]) -(let (?e48 bv140737488355328[64]) -(let (?e49 bv281474976710656[64]) -(let (?e50 bv562949953421312[64]) -(let (?e51 bv1125899906842624[64]) -(let (?e52 bv2251799813685248[64]) -(let (?e53 bv4503599627370496[64]) -(let (?e54 bv9007199254740992[64]) -(let (?e55 bv18014398509481984[64]) -(let (?e56 bv36028797018963968[64]) -(let (?e57 bv72057594037927936[64]) -(let (?e58 bv144115188075855872[64]) -(let (?e59 bv288230376151711744[64]) -(let (?e60 bv576460752303423488[64]) -(let (?e61 bv1152921504606846976[64]) -(let (?e62 bv2305843009213693952[64]) -(let (?e63 bv4611686018427387904[64]) -(let (?e64 bv9223372036854775808[64]) -(let (?e66 (bvadd (bvnot ?e1) ?e1)) -(let (?e67 (bvadd x ?e66)) -(let (?e68 bv1[6]) -(let (?e69 (extract[63:63] ?e67)) -(let (?e70 (bvlshr ?e67 (zero_extend[58] ?e68))) -(let (?e71 (bvlshr (bvnot ?e67) (zero_extend[58] ?e68))) -(let (?e72 (ite (= bv1[1] ?e69) (bvnot ?e71) ?e70)) -(let (?e73 (bvand (bvnot ?e67) (bvnot ?e72))) -(let (?e74 bv2[6]) -(let (?e75 (extract[63:63] (bvnot ?e73))) -(let (?e76 (bvlshr (bvnot ?e73) (zero_extend[58] ?e74))) -(let (?e77 (bvlshr ?e73 (zero_extend[58] ?e74))) -(let (?e78 (ite (= bv1[1] ?e75) (bvnot ?e77) ?e76)) -(let (?e79 (bvand ?e73 (bvnot ?e78))) -(let (?e80 bv3[6]) -(let (?e81 (extract[63:63] (bvnot ?e79))) -(let (?e82 (bvlshr (bvnot ?e79) (zero_extend[58] ?e80))) -(let (?e83 (bvlshr ?e79 (zero_extend[58] ?e80))) -(let (?e84 (ite (= bv1[1] ?e81) (bvnot ?e83) ?e82)) -(let (?e85 (bvand ?e79 (bvnot ?e84))) -(let (?e86 bv4[6]) -(let (?e87 (extract[63:63] (bvnot ?e85))) -(let (?e88 (bvlshr (bvnot ?e85) (zero_extend[58] ?e86))) -(let (?e89 (bvlshr ?e85 (zero_extend[58] ?e86))) -(let (?e90 (ite (= bv1[1] ?e87) (bvnot ?e89) ?e88)) -(let (?e91 (bvand ?e85 (bvnot ?e90))) -(let (?e92 bv5[6]) -(let (?e93 (extract[63:63] (bvnot ?e91))) -(let (?e94 (bvlshr (bvnot ?e91) (zero_extend[58] ?e92))) -(let (?e95 (bvlshr ?e91 (zero_extend[58] ?e92))) -(let (?e96 (ite (= bv1[1] ?e93) (bvnot ?e95) ?e94)) -(let (?e97 (bvand ?e91 (bvnot ?e96))) -(let (?e98 bv6[6]) -(let (?e99 (extract[63:63] (bvnot ?e97))) -(let (?e100 (bvlshr (bvnot ?e97) (zero_extend[58] ?e98))) -(let (?e101 (bvlshr ?e97 (zero_extend[58] ?e98))) -(let (?e102 (ite (= bv1[1] ?e99) (bvnot ?e101) ?e100)) -(let (?e103 (bvand ?e97 (bvnot ?e102))) -(let (?e104 bv7[6]) -(let (?e105 (extract[63:63] (bvnot ?e103))) -(let (?e106 (bvlshr (bvnot ?e103) (zero_extend[58] ?e104))) -(let (?e107 (bvlshr ?e103 (zero_extend[58] ?e104))) -(let (?e108 (ite (= bv1[1] ?e105) (bvnot ?e107) ?e106)) -(let (?e109 (bvand ?e103 (bvnot ?e108))) -(let (?e110 bv8[6]) -(let (?e111 (extract[63:63] (bvnot ?e109))) -(let (?e112 (bvlshr (bvnot ?e109) (zero_extend[58] ?e110))) -(let (?e113 (bvlshr ?e109 (zero_extend[58] ?e110))) -(let (?e114 (ite (= bv1[1] ?e111) (bvnot ?e113) ?e112)) -(let (?e115 (bvand ?e109 (bvnot ?e114))) -(let (?e116 bv9[6]) -(let (?e117 (extract[63:63] (bvnot ?e115))) -(let (?e118 (bvlshr (bvnot ?e115) (zero_extend[58] ?e116))) -(let (?e119 (bvlshr ?e115 (zero_extend[58] ?e116))) -(let (?e120 (ite (= bv1[1] ?e117) (bvnot ?e119) ?e118)) -(let (?e121 (bvand ?e115 (bvnot ?e120))) -(let (?e122 bv10[6]) -(let (?e123 (extract[63:63] (bvnot ?e121))) -(let (?e124 (bvlshr (bvnot ?e121) (zero_extend[58] ?e122))) -(let (?e125 (bvlshr ?e121 (zero_extend[58] ?e122))) -(let (?e126 (ite (= bv1[1] ?e123) (bvnot ?e125) ?e124)) -(let (?e127 (bvand ?e121 (bvnot ?e126))) -(let (?e128 bv11[6]) -(let (?e129 (extract[63:63] (bvnot ?e127))) -(let (?e130 (bvlshr (bvnot ?e127) (zero_extend[58] ?e128))) -(let (?e131 (bvlshr ?e127 (zero_extend[58] ?e128))) -(let (?e132 (ite (= bv1[1] ?e129) (bvnot ?e131) ?e130)) -(let (?e133 (bvand ?e127 (bvnot ?e132))) -(let (?e134 bv12[6]) -(let (?e135 (extract[63:63] (bvnot ?e133))) -(let (?e136 (bvlshr (bvnot ?e133) (zero_extend[58] ?e134))) -(let (?e137 (bvlshr ?e133 (zero_extend[58] ?e134))) -(let (?e138 (ite (= bv1[1] ?e135) (bvnot ?e137) ?e136)) -(let (?e139 (bvand ?e133 (bvnot ?e138))) -(let (?e140 bv13[6]) -(let (?e141 (extract[63:63] (bvnot ?e139))) -(let (?e142 (bvlshr (bvnot ?e139) (zero_extend[58] ?e140))) -(let (?e143 (bvlshr ?e139 (zero_extend[58] ?e140))) -(let (?e144 (ite (= bv1[1] ?e141) (bvnot ?e143) ?e142)) -(let (?e145 (bvand ?e139 (bvnot ?e144))) -(let (?e146 bv14[6]) -(let (?e147 (extract[63:63] (bvnot ?e145))) -(let (?e148 (bvlshr (bvnot ?e145) (zero_extend[58] ?e146))) -(let (?e149 (bvlshr ?e145 (zero_extend[58] ?e146))) -(let (?e150 (ite (= bv1[1] ?e147) (bvnot ?e149) ?e148)) -(let (?e151 (bvand ?e145 (bvnot ?e150))) -(let (?e152 bv15[6]) -(let (?e153 (extract[63:63] (bvnot ?e151))) -(let (?e154 (bvlshr (bvnot ?e151) (zero_extend[58] ?e152))) -(let (?e155 (bvlshr ?e151 (zero_extend[58] ?e152))) -(let (?e156 (ite (= bv1[1] ?e153) (bvnot ?e155) ?e154)) -(let (?e157 (bvand ?e151 (bvnot ?e156))) -(let (?e158 bv16[6]) -(let (?e159 (extract[63:63] (bvnot ?e157))) -(let (?e160 (bvlshr (bvnot ?e157) (zero_extend[58] ?e158))) -(let (?e161 (bvlshr ?e157 (zero_extend[58] ?e158))) -(let (?e162 (ite (= bv1[1] ?e159) (bvnot ?e161) ?e160)) -(let (?e163 (bvand ?e157 (bvnot ?e162))) -(let (?e164 bv17[6]) -(let (?e165 (extract[63:63] (bvnot ?e163))) -(let (?e166 (bvlshr (bvnot ?e163) (zero_extend[58] ?e164))) -(let (?e167 (bvlshr ?e163 (zero_extend[58] ?e164))) -(let (?e168 (ite (= bv1[1] ?e165) (bvnot ?e167) ?e166)) -(let (?e169 (bvand ?e163 (bvnot ?e168))) -(let (?e170 bv18[6]) -(let (?e171 (extract[63:63] (bvnot ?e169))) -(let (?e172 (bvlshr (bvnot ?e169) (zero_extend[58] ?e170))) -(let (?e173 (bvlshr ?e169 (zero_extend[58] ?e170))) -(let (?e174 (ite (= bv1[1] ?e171) (bvnot ?e173) ?e172)) -(let (?e175 (bvand ?e169 (bvnot ?e174))) -(let (?e176 bv19[6]) -(let (?e177 (extract[63:63] (bvnot ?e175))) -(let (?e178 (bvlshr (bvnot ?e175) (zero_extend[58] ?e176))) -(let (?e179 (bvlshr ?e175 (zero_extend[58] ?e176))) -(let (?e180 (ite (= bv1[1] ?e177) (bvnot ?e179) ?e178)) -(let (?e181 (bvand ?e175 (bvnot ?e180))) -(let (?e182 bv20[6]) -(let (?e183 (extract[63:63] (bvnot ?e181))) -(let (?e184 (bvlshr (bvnot ?e181) (zero_extend[58] ?e182))) -(let (?e185 (bvlshr ?e181 (zero_extend[58] ?e182))) -(let (?e186 (ite (= bv1[1] ?e183) (bvnot ?e185) ?e184)) -(let (?e187 (bvand ?e181 (bvnot ?e186))) -(let (?e188 bv21[6]) -(let (?e189 (extract[63:63] (bvnot ?e187))) -(let (?e190 (bvlshr (bvnot ?e187) (zero_extend[58] ?e188))) -(let (?e191 (bvlshr ?e187 (zero_extend[58] ?e188))) -(let (?e192 (ite (= bv1[1] ?e189) (bvnot ?e191) ?e190)) -(let (?e193 (bvand ?e187 (bvnot ?e192))) -(let (?e194 bv22[6]) -(let (?e195 (extract[63:63] (bvnot ?e193))) -(let (?e196 (bvlshr (bvnot ?e193) (zero_extend[58] ?e194))) -(let (?e197 (bvlshr ?e193 (zero_extend[58] ?e194))) -(let (?e198 (ite (= bv1[1] ?e195) (bvnot ?e197) ?e196)) -(let (?e199 (bvand ?e193 (bvnot ?e198))) -(let (?e200 bv23[6]) -(let (?e201 (extract[63:63] (bvnot ?e199))) -(let (?e202 (bvlshr (bvnot ?e199) (zero_extend[58] ?e200))) -(let (?e203 (bvlshr ?e199 (zero_extend[58] ?e200))) -(let (?e204 (ite (= bv1[1] ?e201) (bvnot ?e203) ?e202)) -(let (?e205 (bvand ?e199 (bvnot ?e204))) -(let (?e206 bv24[6]) -(let (?e207 (extract[63:63] (bvnot ?e205))) -(let (?e208 (bvlshr (bvnot ?e205) (zero_extend[58] ?e206))) -(let (?e209 (bvlshr ?e205 (zero_extend[58] ?e206))) -(let (?e210 (ite (= bv1[1] ?e207) (bvnot ?e209) ?e208)) -(let (?e211 (bvand ?e205 (bvnot ?e210))) -(let (?e212 bv25[6]) -(let (?e213 (extract[63:63] (bvnot ?e211))) -(let (?e214 (bvlshr (bvnot ?e211) (zero_extend[58] ?e212))) -(let (?e215 (bvlshr ?e211 (zero_extend[58] ?e212))) -(let (?e216 (ite (= bv1[1] ?e213) (bvnot ?e215) ?e214)) -(let (?e217 (bvand ?e211 (bvnot ?e216))) -(let (?e218 bv26[6]) -(let (?e219 (extract[63:63] (bvnot ?e217))) -(let (?e220 (bvlshr (bvnot ?e217) (zero_extend[58] ?e218))) -(let (?e221 (bvlshr ?e217 (zero_extend[58] ?e218))) -(let (?e222 (ite (= bv1[1] ?e219) (bvnot ?e221) ?e220)) -(let (?e223 (bvand ?e217 (bvnot ?e222))) -(let (?e224 bv27[6]) -(let (?e225 (extract[63:63] (bvnot ?e223))) -(let (?e226 (bvlshr (bvnot ?e223) (zero_extend[58] ?e224))) -(let (?e227 (bvlshr ?e223 (zero_extend[58] ?e224))) -(let (?e228 (ite (= bv1[1] ?e225) (bvnot ?e227) ?e226)) -(let (?e229 (bvand ?e223 (bvnot ?e228))) -(let (?e230 bv28[6]) -(let (?e231 (extract[63:63] (bvnot ?e229))) -(let (?e232 (bvlshr (bvnot ?e229) (zero_extend[58] ?e230))) -(let (?e233 (bvlshr ?e229 (zero_extend[58] ?e230))) -(let (?e234 (ite (= bv1[1] ?e231) (bvnot ?e233) ?e232)) -(let (?e235 (bvand ?e229 (bvnot ?e234))) -(let (?e236 bv29[6]) -(let (?e237 (extract[63:63] (bvnot ?e235))) -(let (?e238 (bvlshr (bvnot ?e235) (zero_extend[58] ?e236))) -(let (?e239 (bvlshr ?e235 (zero_extend[58] ?e236))) -(let (?e240 (ite (= bv1[1] ?e237) (bvnot ?e239) ?e238)) -(let (?e241 (bvand ?e235 (bvnot ?e240))) -(let (?e242 bv30[6]) -(let (?e243 (extract[63:63] (bvnot ?e241))) -(let (?e244 (bvlshr (bvnot ?e241) (zero_extend[58] ?e242))) -(let (?e245 (bvlshr ?e241 (zero_extend[58] ?e242))) -(let (?e246 (ite (= bv1[1] ?e243) (bvnot ?e245) ?e244)) -(let (?e247 (bvand ?e241 (bvnot ?e246))) -(let (?e248 bv31[6]) -(let (?e249 (extract[63:63] (bvnot ?e247))) -(let (?e250 (bvlshr (bvnot ?e247) (zero_extend[58] ?e248))) -(let (?e251 (bvlshr ?e247 (zero_extend[58] ?e248))) -(let (?e252 (ite (= bv1[1] ?e249) (bvnot ?e251) ?e250)) -(let (?e253 (bvand ?e247 (bvnot ?e252))) -(let (?e254 bv32[6]) -(let (?e255 (extract[63:63] (bvnot ?e253))) -(let (?e256 (bvlshr (bvnot ?e253) (zero_extend[58] ?e254))) -(let (?e257 (bvlshr ?e253 (zero_extend[58] ?e254))) -(let (?e258 (ite (= bv1[1] ?e255) (bvnot ?e257) ?e256)) -(let (?e259 (bvand ?e253 (bvnot ?e258))) -(let (?e260 bv33[6]) -(let (?e261 (extract[63:63] (bvnot ?e259))) -(let (?e262 (bvlshr (bvnot ?e259) (zero_extend[58] ?e260))) -(let (?e263 (bvlshr ?e259 (zero_extend[58] ?e260))) -(let (?e264 (ite (= bv1[1] ?e261) (bvnot ?e263) ?e262)) -(let (?e265 (bvand ?e259 (bvnot ?e264))) -(let (?e266 bv34[6]) -(let (?e267 (extract[63:63] (bvnot ?e265))) -(let (?e268 (bvlshr (bvnot ?e265) (zero_extend[58] ?e266))) -(let (?e269 (bvlshr ?e265 (zero_extend[58] ?e266))) -(let (?e270 (ite (= bv1[1] ?e267) (bvnot ?e269) ?e268)) -(let (?e271 (bvand ?e265 (bvnot ?e270))) -(let (?e272 bv35[6]) -(let (?e273 (extract[63:63] (bvnot ?e271))) -(let (?e274 (bvlshr (bvnot ?e271) (zero_extend[58] ?e272))) -(let (?e275 (bvlshr ?e271 (zero_extend[58] ?e272))) -(let (?e276 (ite (= bv1[1] ?e273) (bvnot ?e275) ?e274)) -(let (?e277 (bvand ?e271 (bvnot ?e276))) -(let (?e278 bv36[6]) -(let (?e279 (extract[63:63] (bvnot ?e277))) -(let (?e280 (bvlshr (bvnot ?e277) (zero_extend[58] ?e278))) -(let (?e281 (bvlshr ?e277 (zero_extend[58] ?e278))) -(let (?e282 (ite (= bv1[1] ?e279) (bvnot ?e281) ?e280)) -(let (?e283 (bvand ?e277 (bvnot ?e282))) -(let (?e284 bv37[6]) -(let (?e285 (extract[63:63] (bvnot ?e283))) -(let (?e286 (bvlshr (bvnot ?e283) (zero_extend[58] ?e284))) -(let (?e287 (bvlshr ?e283 (zero_extend[58] ?e284))) -(let (?e288 (ite (= bv1[1] ?e285) (bvnot ?e287) ?e286)) -(let (?e289 (bvand ?e283 (bvnot ?e288))) -(let (?e290 bv38[6]) -(let (?e291 (extract[63:63] (bvnot ?e289))) -(let (?e292 (bvlshr (bvnot ?e289) (zero_extend[58] ?e290))) -(let (?e293 (bvlshr ?e289 (zero_extend[58] ?e290))) -(let (?e294 (ite (= bv1[1] ?e291) (bvnot ?e293) ?e292)) -(let (?e295 (bvand ?e289 (bvnot ?e294))) -(let (?e296 bv39[6]) -(let (?e297 (extract[63:63] (bvnot ?e295))) -(let (?e298 (bvlshr (bvnot ?e295) (zero_extend[58] ?e296))) -(let (?e299 (bvlshr ?e295 (zero_extend[58] ?e296))) -(let (?e300 (ite (= bv1[1] ?e297) (bvnot ?e299) ?e298)) -(let (?e301 (bvand ?e295 (bvnot ?e300))) -(let (?e302 bv40[6]) -(let (?e303 (extract[63:63] (bvnot ?e301))) -(let (?e304 (bvlshr (bvnot ?e301) (zero_extend[58] ?e302))) -(let (?e305 (bvlshr ?e301 (zero_extend[58] ?e302))) -(let (?e306 (ite (= bv1[1] ?e303) (bvnot ?e305) ?e304)) -(let (?e307 (bvand ?e301 (bvnot ?e306))) -(let (?e308 bv41[6]) -(let (?e309 (extract[63:63] (bvnot ?e307))) -(let (?e310 (bvlshr (bvnot ?e307) (zero_extend[58] ?e308))) -(let (?e311 (bvlshr ?e307 (zero_extend[58] ?e308))) -(let (?e312 (ite (= bv1[1] ?e309) (bvnot ?e311) ?e310)) -(let (?e313 (bvand ?e307 (bvnot ?e312))) -(let (?e314 bv42[6]) -(let (?e315 (extract[63:63] (bvnot ?e313))) -(let (?e316 (bvlshr (bvnot ?e313) (zero_extend[58] ?e314))) -(let (?e317 (bvlshr ?e313 (zero_extend[58] ?e314))) -(let (?e318 (ite (= bv1[1] ?e315) (bvnot ?e317) ?e316)) -(let (?e319 (bvand ?e313 (bvnot ?e318))) -(let (?e320 bv43[6]) -(let (?e321 (extract[63:63] (bvnot ?e319))) -(let (?e322 (bvlshr (bvnot ?e319) (zero_extend[58] ?e320))) -(let (?e323 (bvlshr ?e319 (zero_extend[58] ?e320))) -(let (?e324 (ite (= bv1[1] ?e321) (bvnot ?e323) ?e322)) -(let (?e325 (bvand ?e319 (bvnot ?e324))) -(let (?e326 bv44[6]) -(let (?e327 (extract[63:63] (bvnot ?e325))) -(let (?e328 (bvlshr (bvnot ?e325) (zero_extend[58] ?e326))) -(let (?e329 (bvlshr ?e325 (zero_extend[58] ?e326))) -(let (?e330 (ite (= bv1[1] ?e327) (bvnot ?e329) ?e328)) -(let (?e331 (bvand ?e325 (bvnot ?e330))) -(let (?e332 bv45[6]) -(let (?e333 (extract[63:63] (bvnot ?e331))) -(let (?e334 (bvlshr (bvnot ?e331) (zero_extend[58] ?e332))) -(let (?e335 (bvlshr ?e331 (zero_extend[58] ?e332))) -(let (?e336 (ite (= bv1[1] ?e333) (bvnot ?e335) ?e334)) -(let (?e337 (bvand ?e331 (bvnot ?e336))) -(let (?e338 bv46[6]) -(let (?e339 (extract[63:63] (bvnot ?e337))) -(let (?e340 (bvlshr (bvnot ?e337) (zero_extend[58] ?e338))) -(let (?e341 (bvlshr ?e337 (zero_extend[58] ?e338))) -(let (?e342 (ite (= bv1[1] ?e339) (bvnot ?e341) ?e340)) -(let (?e343 (bvand ?e337 (bvnot ?e342))) -(let (?e344 bv47[6]) -(let (?e345 (extract[63:63] (bvnot ?e343))) -(let (?e346 (bvlshr (bvnot ?e343) (zero_extend[58] ?e344))) -(let (?e347 (bvlshr ?e343 (zero_extend[58] ?e344))) -(let (?e348 (ite (= bv1[1] ?e345) (bvnot ?e347) ?e346)) -(let (?e349 (bvand ?e343 (bvnot ?e348))) -(let (?e350 bv48[6]) -(let (?e351 (extract[63:63] (bvnot ?e349))) -(let (?e352 (bvlshr (bvnot ?e349) (zero_extend[58] ?e350))) -(let (?e353 (bvlshr ?e349 (zero_extend[58] ?e350))) -(let (?e354 (ite (= bv1[1] ?e351) (bvnot ?e353) ?e352)) -(let (?e355 (bvand ?e349 (bvnot ?e354))) -(let (?e356 bv49[6]) -(let (?e357 (extract[63:63] (bvnot ?e355))) -(let (?e358 (bvlshr (bvnot ?e355) (zero_extend[58] ?e356))) -(let (?e359 (bvlshr ?e355 (zero_extend[58] ?e356))) -(let (?e360 (ite (= bv1[1] ?e357) (bvnot ?e359) ?e358)) -(let (?e361 (bvand ?e355 (bvnot ?e360))) -(let (?e362 bv50[6]) -(let (?e363 (extract[63:63] (bvnot ?e361))) -(let (?e364 (bvlshr (bvnot ?e361) (zero_extend[58] ?e362))) -(let (?e365 (bvlshr ?e361 (zero_extend[58] ?e362))) -(let (?e366 (ite (= bv1[1] ?e363) (bvnot ?e365) ?e364)) -(let (?e367 (bvand ?e361 (bvnot ?e366))) -(let (?e368 bv51[6]) -(let (?e369 (extract[63:63] (bvnot ?e367))) -(let (?e370 (bvlshr (bvnot ?e367) (zero_extend[58] ?e368))) -(let (?e371 (bvlshr ?e367 (zero_extend[58] ?e368))) -(let (?e372 (ite (= bv1[1] ?e369) (bvnot ?e371) ?e370)) -(let (?e373 (bvand ?e367 (bvnot ?e372))) -(let (?e374 bv52[6]) -(let (?e375 (extract[63:63] (bvnot ?e373))) -(let (?e376 (bvlshr (bvnot ?e373) (zero_extend[58] ?e374))) -(let (?e377 (bvlshr ?e373 (zero_extend[58] ?e374))) -(let (?e378 (ite (= bv1[1] ?e375) (bvnot ?e377) ?e376)) -(let (?e379 (bvand ?e373 (bvnot ?e378))) -(let (?e380 bv53[6]) -(let (?e381 (extract[63:63] (bvnot ?e379))) -(let (?e382 (bvlshr (bvnot ?e379) (zero_extend[58] ?e380))) -(let (?e383 (bvlshr ?e379 (zero_extend[58] ?e380))) -(let (?e384 (ite (= bv1[1] ?e381) (bvnot ?e383) ?e382)) -(let (?e385 (bvand ?e379 (bvnot ?e384))) -(let (?e386 bv54[6]) -(let (?e387 (extract[63:63] (bvnot ?e385))) -(let (?e388 (bvlshr (bvnot ?e385) (zero_extend[58] ?e386))) -(let (?e389 (bvlshr ?e385 (zero_extend[58] ?e386))) -(let (?e390 (ite (= bv1[1] ?e387) (bvnot ?e389) ?e388)) -(let (?e391 (bvand ?e385 (bvnot ?e390))) -(let (?e392 bv55[6]) -(let (?e393 (extract[63:63] (bvnot ?e391))) -(let (?e394 (bvlshr (bvnot ?e391) (zero_extend[58] ?e392))) -(let (?e395 (bvlshr ?e391 (zero_extend[58] ?e392))) -(let (?e396 (ite (= bv1[1] ?e393) (bvnot ?e395) ?e394)) -(let (?e397 (bvand ?e391 (bvnot ?e396))) -(let (?e398 bv56[6]) -(let (?e399 (extract[63:63] (bvnot ?e397))) -(let (?e400 (bvlshr (bvnot ?e397) (zero_extend[58] ?e398))) -(let (?e401 (bvlshr ?e397 (zero_extend[58] ?e398))) -(let (?e402 (ite (= bv1[1] ?e399) (bvnot ?e401) ?e400)) -(let (?e403 (bvand ?e397 (bvnot ?e402))) -(let (?e404 bv57[6]) -(let (?e405 (extract[63:63] (bvnot ?e403))) -(let (?e406 (bvlshr (bvnot ?e403) (zero_extend[58] ?e404))) -(let (?e407 (bvlshr ?e403 (zero_extend[58] ?e404))) -(let (?e408 (ite (= bv1[1] ?e405) (bvnot ?e407) ?e406)) -(let (?e409 (bvand ?e403 (bvnot ?e408))) -(let (?e410 bv58[6]) -(let (?e411 (extract[63:63] (bvnot ?e409))) -(let (?e412 (bvlshr (bvnot ?e409) (zero_extend[58] ?e410))) -(let (?e413 (bvlshr ?e409 (zero_extend[58] ?e410))) -(let (?e414 (ite (= bv1[1] ?e411) (bvnot ?e413) ?e412)) -(let (?e415 (bvand ?e409 (bvnot ?e414))) -(let (?e416 bv59[6]) -(let (?e417 (extract[63:63] (bvnot ?e415))) -(let (?e418 (bvlshr (bvnot ?e415) (zero_extend[58] ?e416))) -(let (?e419 (bvlshr ?e415 (zero_extend[58] ?e416))) -(let (?e420 (ite (= bv1[1] ?e417) (bvnot ?e419) ?e418)) -(let (?e421 (bvand ?e415 (bvnot ?e420))) -(let (?e422 bv60[6]) -(let (?e423 (extract[63:63] (bvnot ?e421))) -(let (?e424 (bvlshr (bvnot ?e421) (zero_extend[58] ?e422))) -(let (?e425 (bvlshr ?e421 (zero_extend[58] ?e422))) -(let (?e426 (ite (= bv1[1] ?e423) (bvnot ?e425) ?e424)) -(let (?e427 (bvand ?e421 (bvnot ?e426))) -(let (?e428 bv61[6]) -(let (?e429 (extract[63:63] (bvnot ?e427))) -(let (?e430 (bvlshr (bvnot ?e427) (zero_extend[58] ?e428))) -(let (?e431 (bvlshr ?e427 (zero_extend[58] ?e428))) -(let (?e432 (ite (= bv1[1] ?e429) (bvnot ?e431) ?e430)) -(let (?e433 (bvand ?e427 (bvnot ?e432))) -(let (?e434 bv62[6]) -(let (?e435 (extract[63:63] (bvnot ?e433))) -(let (?e436 (bvlshr (bvnot ?e433) (zero_extend[58] ?e434))) -(let (?e437 (bvlshr ?e433 (zero_extend[58] ?e434))) -(let (?e438 (ite (= bv1[1] ?e435) (bvnot ?e437) ?e436)) -(let (?e439 (bvand ?e433 (bvnot ?e438))) -(let (?e440 bv63[6]) -(let (?e441 (extract[63:63] (bvnot ?e439))) -(let (?e442 (bvlshr (bvnot ?e439) (zero_extend[58] ?e440))) -(let (?e443 (bvlshr ?e439 (zero_extend[58] ?e440))) -(let (?e444 (ite (= bv1[1] ?e441) (bvnot ?e443) ?e442)) -(let (?e445 (bvand ?e439 (bvnot ?e444))) -(let (?e446 (bvadd ?e1 (bvnot ?e445))) -(let (?e447 bv0[1]) -(let (?e448 (ite (= ?e1 ?e446) bv1[1] bv0[1])) -(let (?e449 (bvand (bvnot ?e447) (bvnot ?e448))) -(let (?e450 (ite (= ?e2 ?e446) bv1[1] bv0[1])) -(let (?e451 (bvand ?e449 (bvnot ?e450))) -(let (?e452 (ite (= ?e3 ?e446) bv1[1] bv0[1])) -(let (?e453 (bvand ?e451 (bvnot ?e452))) -(let (?e454 (ite (= ?e4 ?e446) bv1[1] bv0[1])) -(let (?e455 (bvand ?e453 (bvnot ?e454))) -(let (?e456 (ite (= ?e5 ?e446) bv1[1] bv0[1])) -(let (?e457 (bvand ?e455 (bvnot ?e456))) -(let (?e458 (ite (= ?e6 ?e446) bv1[1] bv0[1])) -(let (?e459 (bvand ?e457 (bvnot ?e458))) -(let (?e460 (ite (= ?e7 ?e446) bv1[1] bv0[1])) -(let (?e461 (bvand ?e459 (bvnot ?e460))) -(let (?e462 (ite (= ?e8 ?e446) bv1[1] bv0[1])) -(let (?e463 (bvand ?e461 (bvnot ?e462))) -(let (?e464 (ite (= ?e9 ?e446) bv1[1] bv0[1])) -(let (?e465 (bvand ?e463 (bvnot ?e464))) -(let (?e466 (ite (= ?e10 ?e446) bv1[1] bv0[1])) -(let (?e467 (bvand ?e465 (bvnot ?e466))) -(let (?e468 (ite (= ?e11 ?e446) bv1[1] bv0[1])) -(let (?e469 (bvand ?e467 (bvnot ?e468))) -(let (?e470 (ite (= ?e12 ?e446) bv1[1] bv0[1])) -(let (?e471 (bvand ?e469 (bvnot ?e470))) -(let (?e472 (ite (= ?e13 ?e446) bv1[1] bv0[1])) -(let (?e473 (bvand ?e471 (bvnot ?e472))) -(let (?e474 (ite (= ?e14 ?e446) bv1[1] bv0[1])) -(let (?e475 (bvand ?e473 (bvnot ?e474))) -(let (?e476 (ite (= ?e15 ?e446) bv1[1] bv0[1])) -(let (?e477 (bvand ?e475 (bvnot ?e476))) -(let (?e478 (ite (= ?e16 ?e446) bv1[1] bv0[1])) -(let (?e479 (bvand ?e477 (bvnot ?e478))) -(let (?e480 (ite (= ?e17 ?e446) bv1[1] bv0[1])) -(let (?e481 (bvand ?e479 (bvnot ?e480))) -(let (?e482 (ite (= ?e18 ?e446) bv1[1] bv0[1])) -(let (?e483 (bvand ?e481 (bvnot ?e482))) -(let (?e484 (ite (= ?e19 ?e446) bv1[1] bv0[1])) -(let (?e485 (bvand ?e483 (bvnot ?e484))) -(let (?e486 (ite (= ?e20 ?e446) bv1[1] bv0[1])) -(let (?e487 (bvand ?e485 (bvnot ?e486))) -(let (?e488 (ite (= ?e21 ?e446) bv1[1] bv0[1])) -(let (?e489 (bvand ?e487 (bvnot ?e488))) -(let (?e490 (ite (= ?e22 ?e446) bv1[1] bv0[1])) -(let (?e491 (bvand ?e489 (bvnot ?e490))) -(let (?e492 (ite (= ?e23 ?e446) bv1[1] bv0[1])) -(let (?e493 (bvand ?e491 (bvnot ?e492))) -(let (?e494 (ite (= ?e24 ?e446) bv1[1] bv0[1])) -(let (?e495 (bvand ?e493 (bvnot ?e494))) -(let (?e496 (ite (= ?e25 ?e446) bv1[1] bv0[1])) -(let (?e497 (bvand ?e495 (bvnot ?e496))) -(let (?e498 (ite (= ?e26 ?e446) bv1[1] bv0[1])) -(let (?e499 (bvand ?e497 (bvnot ?e498))) -(let (?e500 (ite (= ?e27 ?e446) bv1[1] bv0[1])) -(let (?e501 (bvand ?e499 (bvnot ?e500))) -(let (?e502 (ite (= ?e28 ?e446) bv1[1] bv0[1])) -(let (?e503 (bvand ?e501 (bvnot ?e502))) -(let (?e504 (ite (= ?e29 ?e446) bv1[1] bv0[1])) -(let (?e505 (bvand ?e503 (bvnot ?e504))) -(let (?e506 (ite (= ?e30 ?e446) bv1[1] bv0[1])) -(let (?e507 (bvand ?e505 (bvnot ?e506))) -(let (?e508 (ite (= ?e31 ?e446) bv1[1] bv0[1])) -(let (?e509 (bvand ?e507 (bvnot ?e508))) -(let (?e510 (ite (= ?e32 ?e446) bv1[1] bv0[1])) -(let (?e511 (bvand ?e509 (bvnot ?e510))) -(let (?e512 (ite (= ?e33 ?e446) bv1[1] bv0[1])) -(let (?e513 (bvand ?e511 (bvnot ?e512))) -(let (?e514 (ite (= ?e34 ?e446) bv1[1] bv0[1])) -(let (?e515 (bvand ?e513 (bvnot ?e514))) -(let (?e516 (ite (= ?e35 ?e446) bv1[1] bv0[1])) -(let (?e517 (bvand ?e515 (bvnot ?e516))) -(let (?e518 (ite (= ?e36 ?e446) bv1[1] bv0[1])) -(let (?e519 (bvand ?e517 (bvnot ?e518))) -(let (?e520 (ite (= ?e37 ?e446) bv1[1] bv0[1])) -(let (?e521 (bvand ?e519 (bvnot ?e520))) -(let (?e522 (ite (= ?e38 ?e446) bv1[1] bv0[1])) -(let (?e523 (bvand ?e521 (bvnot ?e522))) -(let (?e524 (ite (= ?e39 ?e446) bv1[1] bv0[1])) -(let (?e525 (bvand ?e523 (bvnot ?e524))) -(let (?e526 (ite (= ?e40 ?e446) bv1[1] bv0[1])) -(let (?e527 (bvand ?e525 (bvnot ?e526))) -(let (?e528 (ite (= ?e41 ?e446) bv1[1] bv0[1])) -(let (?e529 (bvand ?e527 (bvnot ?e528))) -(let (?e530 (ite (= ?e42 ?e446) bv1[1] bv0[1])) -(let (?e531 (bvand ?e529 (bvnot ?e530))) -(let (?e532 (ite (= ?e43 ?e446) bv1[1] bv0[1])) -(let (?e533 (bvand ?e531 (bvnot ?e532))) -(let (?e534 (ite (= ?e44 ?e446) bv1[1] bv0[1])) -(let (?e535 (bvand ?e533 (bvnot ?e534))) -(let (?e536 (ite (= ?e45 ?e446) bv1[1] bv0[1])) -(let (?e537 (bvand ?e535 (bvnot ?e536))) -(let (?e538 (ite (= ?e46 ?e446) bv1[1] bv0[1])) -(let (?e539 (bvand ?e537 (bvnot ?e538))) -(let (?e540 (ite (= ?e47 ?e446) bv1[1] bv0[1])) -(let (?e541 (bvand ?e539 (bvnot ?e540))) -(let (?e542 (ite (= ?e48 ?e446) bv1[1] bv0[1])) -(let (?e543 (bvand ?e541 (bvnot ?e542))) -(let (?e544 (ite (= ?e49 ?e446) bv1[1] bv0[1])) -(let (?e545 (bvand ?e543 (bvnot ?e544))) -(let (?e546 (ite (= ?e50 ?e446) bv1[1] bv0[1])) -(let (?e547 (bvand ?e545 (bvnot ?e546))) -(let (?e548 (ite (= ?e51 ?e446) bv1[1] bv0[1])) -(let (?e549 (bvand ?e547 (bvnot ?e548))) -(let (?e550 (ite (= ?e52 ?e446) bv1[1] bv0[1])) -(let (?e551 (bvand ?e549 (bvnot ?e550))) -(let (?e552 (ite (= ?e53 ?e446) bv1[1] bv0[1])) -(let (?e553 (bvand ?e551 (bvnot ?e552))) -(let (?e554 (ite (= ?e54 ?e446) bv1[1] bv0[1])) -(let (?e555 (bvand ?e553 (bvnot ?e554))) -(let (?e556 (ite (= ?e55 ?e446) bv1[1] bv0[1])) -(let (?e557 (bvand ?e555 (bvnot ?e556))) -(let (?e558 (ite (= ?e56 ?e446) bv1[1] bv0[1])) -(let (?e559 (bvand ?e557 (bvnot ?e558))) -(let (?e560 (ite (= ?e57 ?e446) bv1[1] bv0[1])) -(let (?e561 (bvand ?e559 (bvnot ?e560))) -(let (?e562 (ite (= ?e58 ?e446) bv1[1] bv0[1])) -(let (?e563 (bvand ?e561 (bvnot ?e562))) -(let (?e564 (ite (= ?e59 ?e446) bv1[1] bv0[1])) -(let (?e565 (bvand ?e563 (bvnot ?e564))) -(let (?e566 (ite (= ?e60 ?e446) bv1[1] bv0[1])) -(let (?e567 (bvand ?e565 (bvnot ?e566))) -(let (?e568 (ite (= ?e61 ?e446) bv1[1] bv0[1])) -(let (?e569 (bvand ?e567 (bvnot ?e568))) -(let (?e570 (ite (= ?e62 ?e446) bv1[1] bv0[1])) -(let (?e571 (bvand ?e569 (bvnot ?e570))) -(let (?e572 (ite (= ?e63 ?e446) bv1[1] bv0[1])) -(let (?e573 (bvand ?e571 (bvnot ?e572))) -(let (?e574 (ite (= ?e64 ?e446) bv1[1] bv0[1])) -(let (?e575 (bvand ?e573 (bvnot ?e574))) -(let (?e576 (ite (bvult ?e446 x) bv1[1] bv0[1])) -(let (?e577 (bvand (bvnot ?e575) (bvnot ?e576))) -(let (?e578 (bvlshr ?e446 (zero_extend[58] ?e68))) -(let (?e579 (extract[63:63] ?e578)) -(let (?e580 (extract[63:63] x)) -(let (?e581 (extract[62:0] ?e578)) -(let (?e582 (extract[62:0] x)) -(let (?e583 (ite (bvult ?e581 ?e582) bv1[1] bv0[1])) -(let (?e584 (bvand ?e579 (bvnot ?e580))) -(let (?e585 (bvand (bvnot ?e579) (bvnot ?e580))) -(let (?e586 (bvand ?e579 ?e580)) -(let (?e587 (bvand ?e583 ?e585)) -(let (?e588 (bvand ?e583 ?e586)) -(let (?e589 (bvand (bvnot ?e587) (bvnot ?e588))) -(let (?e590 (bvand (bvnot ?e584) ?e589)) -(let (?e591 (bvand ?e577 (bvnot ?e590))) -(let (?e592 (extract[63:63] ?e1)) -(let (?e593 (extract[62:0] ?e1)) -(let (?e594 (ite (bvult ?e582 ?e593) bv1[1] bv0[1])) -(let (?e595 (bvand ?e580 (bvnot ?e592))) -(let (?e596 (bvand (bvnot ?e580) (bvnot ?e592))) -(let (?e597 (bvand ?e580 ?e592)) -(let (?e598 (bvand ?e594 ?e596)) -(let (?e599 (bvand ?e594 ?e597)) -(let (?e600 (bvand (bvnot ?e598) (bvnot ?e599))) -(let (?e601 (bvand (bvnot ?e595) ?e600)) -(let (?e602 (bvand (bvnot ?e591) ?e601)) -(not (= ?e602 bv0[1])) -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -- 2.47.3