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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 9aca00061a1dae1ded91120b8b797025324b3ba9..3a0dd7878f2a74a91fdc10cd564a9cd5059adb1f 100644 (file)
--- 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());
         }