From 990e0bfc3087f0b7fd1adf8d4d1858ad6b6fc0ec Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 7 Jan 2012 15:17:33 +0000
Subject: [PATCH] Fix. Code that isn't enabled without a special config. option
 was broken.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1478 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/BitBlaster.cpp | 19 ++-----------------
 1 file changed, 2 insertions(+), 17 deletions(-)

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 9aca000..3a0dd78 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1402,6 +1402,7 @@ namespace BEEV
         ms.print();
         }
 
+      vector<BBNode> prior;
       for (int i = 0; i < bitWidth; i++)
         {
         if (debug_bounds)
@@ -1410,27 +1411,11 @@ namespace BEEV
           cerr << "[" << ms.columnL[i] << ":" << ms.columnH[i] << "][" << ms.sumL[i] << ":" << ms.sumH[i] << "]";
           }
 
-        if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
-          {
-          if (debug_bounds)
-            cerr << "S";
-          // sorting network.
-
-          //int width = std::min(ms.sumH[i]+1, (signed)products[i].size());
           vector<BBNode> output;
-          vector<BBNode> prior;
+
           mult_SortingNetwork(toConjoinToTop, products[i], output, prior, ms.sumL[i], ms.sumH[i]);
           prior = output;
 
-          }
-        else // addition network.
-          {
-          if (debug_bounds)
-            cerr << "A";
-
-          buildAdditionNetworkResult(products[i], products[i+1], toConjoinToTop, (i + 1 == bitWidth), 0 == ms.sumH[i]);
-          }
-
         assert(products[i].size() == 1);
         result.push_back(products[i].back());
         }
-- 
2.47.3