From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 2 Jan 2012 13:24:37 +0000 (+0000)
Subject: Bugfix. The previous checkin broke multiplication.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=bd9da7cc4c53aae5fc8fbcac71a4ef203b9d993c;p=francis%2Fstp.git

Bugfix. The previous checkin broke multiplication.

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 76c334f..93d124e 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1150,6 +1150,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BB
   BBNodeVec results;
   for (int i = 0; i < bitWidth; i++)
     {
+        if (i+1 != bitWidth)
               buildAdditionNetworkResult(&(products[i]), &(products[i+1]), support, bitWidth, i);
           else
               buildAdditionNetworkResult(&(products[i]), NULL, support, bitWidth, i);
@@ -1165,11 +1166,11 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BB
 // Use full adders to create an addition network that adds together each of the
 // partial products.
 template <class BBNode, class BBNodeManagerT>
-void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>* from_, stack<BBNode>* to_, set<BBNode>& support,
+void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>* from_, stack<BBNode>* to, set<BBNode>& support,
 		const int bitWidth, const int i, const int minTrue, const int maxTrue )
 {
-    stack<BBNode> from = *from_;
-    stack<BBNode> to = *to_;
+    stack<BBNode>& from = *from_;
+
 
     while (from.size() >= 2) {
               BBNode c;
@@ -1229,8 +1230,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>
              }
              else if (i + 1 != bitWidth && carry != BBFalse)
              {
-                     assert(to != NULL);
-                     to.push(carry);
+                     to->push(carry);
              }
       }
       if (0==from.size())