Important BugFix. r230 introduced an off-by-one error in the left-shift circuit that...

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

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 42555a3d21df14c50793d6e70fc3bae659746622..ff70261921accd0b0fe47c50c9a1b553bf67fa43 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -121,7 +121,7 @@ namespace BEEV
                   
                   int shift_amount = 1 << i;
                   
-                  for (signed int j = width - 1; j > 0; j--)
+                  for (signed int j = width - 1; j >= 0; j--)
                     {
                       if (j < shift_amount)
                         {