Fix. Another broken assertion.

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index ca438ce964b45c5b94ff162e19c5d66047d9832d..c43ded203f6a7bd179c38019369fbf8107ca7109 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1253,7 +1253,7 @@ namespace BEEV
         results.push_back(products[i].back());
         }
 
-      assert(products[bitWidth].size() ==0); // i+1 is defined but should never be used.
+      assert(products[bitWidth].size() ==0); // products[bitwidth] is defined but should never be used.
       assert(results.size() == ((unsigned)bitWidth));
       return results;
     }
@@ -1773,12 +1773,12 @@ namespace BEEV
         return buildAdditionNetworkResult(products.data(), support, n);
         }
       else if (multiplication_variant == "5")
-        {
-        if (!statsFound(n))
-          {
-          mult_Booth(_x, _y, support, n[0], n[1], products.data(), n);
-          return buildAdditionNetworkResult(products.data(), support, n);
-          }
+              {
+              if (!statsFound(n) || !multiplication_upper_bound)
+                {
+                mult_Booth(_x, _y, support, n[0], n[1], products.data(), n);
+                return buildAdditionNetworkResult(products.data(), support, n);
+                }
 
         mult_allPairs(x, y, support, products.data());
         return multWithBounds(n, products.data(), support);