From d12c1897513c0dcc2c4fe4bcd5adf29a55a58eda Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 9 Jan 2012 13:56:36 +0000 Subject: [PATCH] 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 --- src/to-sat/BitBlaster.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index ca438ce..c43ded2 100644 --- 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); -- 2.47.3