Fix off-by-one in bitvector right shift.

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

diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp
index 57256d8e8e97714efc0b1512895d77d652aa941f..c9f50237fcde7419d32bc403833719c624d88375 100644 (file)
--- a/AST/BitBlast.cpp
+++ b/AST/BitBlast.cpp
@@ -149,7 +149,7 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
            
            bool done = false;
            
-           for (unsigned int j=0; j < temp_result.size()-1; j++)
+           for (unsigned int j=0; j < temp_result.size(); j++)
              {
                if (j + shift_amount >= temp_result.size())
                  temp_result[j] = CreateSimpForm(ITE, bbarg2[i],ASTFalse,temp_result[j]);

diff --git a/AST/ToCNF.cpp b/AST/ToCNF.cpp
index 0857e7046e5f653e5b6f2c34fb298a0dff80cf5b..59d2d21bd8ceb1df15cff1100275b4f16e5dcaef 100644 (file)
--- a/AST/ToCNF.cpp
+++ b/AST/ToCNF.cpp
@@ -1541,6 +1541,9 @@ private:
     ASTNode BBFormula = BBForm(q);
     CNFMgr* cm = new CNFMgr(this);
     ClauseList* cl = cm->convertToCNF(BBFormula);
+    if(stats)
+      cerr << "Number of clauses:" << cl->size() << endl;
+       //PrintClauseList(cout, *cl);
     bool sat = toSATandSolve(newS,*cl);    
     cm->DELETE(cl);
     delete cm;

diff --git a/broken/BROKEN b/broken/BROKEN
index 43e84ac6b22d6a39e8065b8d81df0d3bcfa4c4f5..be316785632d13e6d803fb7c350adbb83001003a 100644 (file)
--- a/broken/BROKEN
+++ b/broken/BROKEN
@@ -1,9 +1,5 @@
-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.
+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
new file mode 100644 (file)
index 0000000..a87e621
--- /dev/null
+++ b/broken/fixed/little.smt
@@ -0,0 +1,22 @@
+(
+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/little.smt b/broken/little.smt
deleted file mode 100644 (file)
index da91d12..0000000
--- a/broken/little.smt
+++ /dev/null
@@ -1,18 +0,0 @@
-(
-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]))
-
-)
-