From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 13 Jan 2009 14:02:57 +0000 (+0000)
Subject: Fix off-by-one in bitvector right shift.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ed5230cabd0a76852917df08e6e71b15ef4ba9ad;p=francis%2Fstp.git

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 57256d8..c9f5023 100644
--- 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 0857e70..59d2d21 100644
--- 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 43e84ac..be31678 100644
--- 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
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
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]))
-
-)
-