Right shift by a variable amount. Add two broken SMT files.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@53 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp
index 7ead02caf1601e6c4ffd7a0fae55899a174c4f72..57256d8e8e97714efc0b1512895d77d652aa941f 100644 (file)
--- a/AST/BitBlast.cpp
+++ b/AST/BitBlast.cpp
@@ -107,7 +107,7 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
                                else
                                        temp_result[j] = CreateSimpForm(ITE, bbarg2[i],temp_result[j-shift_amount],temp_result[j]);
                                
-                               // want it to stop after doing 0, but subtracting 1 from j makes it very big. 
+               // want the loop to finish after j=0, but when j=0, j-1 == MAX_INT. Hence this weird idiom.
                                if (j ==0)
                                        done = true;
                        }
@@ -134,8 +134,43 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
       }
      else
        {
-               FatalError("Not implemented shift right by unk. value.");
-               }
+       // Barrel shifter
+       const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
+       const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();  
+       
+       ASTVec temp_result(bbarg1);
+       
+       for (unsigned int i =0; i < bbarg2.size(); i++)
+         {
+           if (bbarg2[i] == ASTFalse) 
+             continue;  // Not shifting by anything.
+           
+           unsigned int shift_amount = 1 << i;
+           
+           bool done = false;
+           
+           for (unsigned int j=0; j < temp_result.size()-1; j++)
+             {
+               if (j + shift_amount >= temp_result.size())
+                 temp_result[j] = CreateSimpForm(ITE, bbarg2[i],ASTFalse,temp_result[j]);
+               else
+                 temp_result[j] = CreateSimpForm(ITE, bbarg2[i],temp_result[j+shift_amount],temp_result[j]);
+               
+               if (j ==0)
+                 done = true;
+             }
+         }
+
+       
+       result =  CreateNode(BOOLVEC, temp_result);
+
+       /*      cerr << result << endl;
+       cerr << term[0] << endl;
+       cerr << term[1] << endl;
+       cerr << "right shift. Node size is:" << NodeSize(result) << endl;
+       cerr << "input size: " << NodeSize(term[0]) << " " << NodeSize(term[1]) << endl;
+       */
+       }
    }
        break;
    

diff --git a/broken/BROKEN b/broken/BROKEN
new file mode 100644 (file)
index 0000000..43e84ac
--- /dev/null
+++ b/broken/BROKEN
@@ -0,0 +1,9 @@
+little.smt
+---
+* Ends without achieving a result. Not sure why?
+
+
+nextpoweroftwo064.smt
+---
+With optimizations disabled it finishes in 7.3 seconds (on my machine). With optimizations enabled. Uses lots of memory when converting to CNF.
+

diff --git a/broken/little.smt b/broken/little.smt
new file mode 100644 (file)
index 0000000..da91d12
--- /dev/null
+++ b/broken/little.smt
@@ -0,0 +1,18 @@
+(
+benchmark temp20.smt
+:source {Minkeyrink Solver}
+:status unsat
+:difficulty {1}
+:category {industrial}
+:logic QF_BV
+:extrafuns ((sym1 BitVec[4]))
+:extrafuns ((sym2 BitVec[1]))
+:extrafuns ((sym3 BitVec[4]))
+
+:assumption (= (bvlshr sym1 (zero_extend[3] sym2)) sym3)
+:assumption (= (bvlshr sym3(zero_extend[3] sym2)) sym1)
+:assumption (not (= sym2 bv0[1]))
+:assumption (not (= sym1 bv0[4]))
+
+)
+

diff --git a/broken/nextpoweroftwo064.smt b/broken/nextpoweroftwo064.smt
new file mode 100644 (file)
index 0000000..977a945
--- /dev/null
+++ b/broken/nextpoweroftwo064.smt
@@ -0,0 +1,628 @@
+(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]))
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

diff --git a/parser/main.cpp b/parser/main.cpp
index 4f1034ef2817a7f297d6aa93538c994f657f4c20..3a0f908aa956bc71a7ed03372bc6b33ac815b525 100644 (file)
--- a/parser/main.cpp
+++ b/parser/main.cpp
@@ -153,7 +153,7 @@ int main(int argc, char ** argv) {
       }
       if(argv[i][2]) {
        fprintf(stderr, "Multiple character options are not allowed.\n");
-       fprintf(stderr, "(-ab is not an abbreviation for -a -b)\n");
+       fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n");
        fprintf(stderr,usage,prog);
        cout << helpstring;
        return -1;

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index 6e4941452105a8eab3e30eaeb25ad2c557f1620a..68abb935f3b490423322270ba8f87895bde898fa 100644 (file)
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -1406,7 +1406,11 @@ namespace BEEV {
 
    case BVZX:
       {
-       output = CreateTerm(BVZX,inputValueWidth,SimplifyTerm(inputterm[0]),inputterm[1]);
+       ASTNode a0 = SimplifyTerm(inputterm[0]);
+       if (a0.GetKind() ==  BVCONST)
+         output = BVConstEvaluator(CreateTerm(BVZX,inputValueWidth,a0,inputterm[1]));
+       else
+         output = CreateTerm(BVZX,inputValueWidth,a0,inputterm[1]);
       }
        break;
 
@@ -1647,6 +1651,8 @@ namespace BEEV {
     //memoize
     UpdateSimplifyMap(inputterm,output,false);
     //cerr << "SimplifyTerm: output" << output << endl;
+    // CheckSimplifyInvariant(inputterm,output);
+
     return output;
   } //end of SimplifyTerm()
 
@@ -2271,17 +2277,14 @@ namespace BEEV {
   //At the end of each simplification call, we want the output to be
   //always smaller or equal to the input in size.
   void BeevMgr::CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output) {
-    //Don't do the check in optimized mode
-    if(optimize)
-      return;
 
-    if(NodeSize(a,true) < NodeSize(output,true)) {
+    if(NodeSize(a,true) + 1  < NodeSize(output,true)) {
       cerr << "lhs := " << a << endl;
       cerr << "NodeSize of lhs is: " << NodeSize(a, true) << endl;
       cerr << endl;
       cerr << "rhs := " << output << endl;
       cerr << "NodeSize of rhs is: " << NodeSize(output, true) << endl;
-      FatalError("SimplifyFormula: The nodesize shoudl decrease from lhs to rhs: ",ASTUndefined);
+      //  FatalError("SimplifyFormula: The nodesize shoudl decrease from lhs to rhs: ",ASTUndefined);
     }
   }