+++ /dev/null
-(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]))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
projects / francis / stp.git / commitdiff