From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 May 2011 04:15:15 +0000 (+0000)
Subject: Fix. Creating the node (v + v), where v is greater than 64 bits would fail.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1f821341f6abbc55d4ee6c2e0cf8c1a92a4b0454;p=francis%2Fstp.git

Fix. Creating the node (v + v), where v is greater than 64 bits would fail.



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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 2310e73..dd3836e 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -764,7 +764,7 @@ ASTNode SimplifyingNodeFactory::plusRules(const ASTNode& n0, const ASTNode& n1)
   else if (width == 1 && n0 == n1)
     result = bm.CreateZeroConst(1);
   else if (n0 == n1)
-    result = NodeFactory::CreateTerm(BEEV::BVMULT, width, bm.CreateBVConst(width,2), n0);
+    result = NodeFactory::CreateTerm(BEEV::BVMULT, width, bm.CreateBVConst(string("2"), 10, width), n0);
   else if (n0.GetKind() == BEEV::BVUMINUS  && n1 == n0[0])
     result = bm.CreateZeroConst(width);
   else if (n1.GetKind() == BEEV::BVPLUS && n1[1].GetKind() == BEEV::BVUMINUS && n0 == n1[1][0] && n1.Degree() ==2 )
diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index ce86865..750f542 100644
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -266,7 +266,7 @@ namespace BEEV
     return n;
   }
 
-  ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width)
+  ASTNode STPMgr::CreateBVConst(string strval, int base, int bit_width)
   {
     assert (bit_width > 0);
 
diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 24aefb8..e13a72a 100644
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -276,7 +276,7 @@ namespace BEEV
     ASTNode CreateZeroConst(unsigned int width);
     ASTNode CreateBVConst(CBV bv, unsigned width);
     ASTNode CreateBVConst(const char *strval, int base);
-    ASTNode CreateBVConst(string& strval, int base, int bit_width);    
+    ASTNode CreateBVConst(string strval, int base, int bit_width);
     ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst);
     ASTNode charToASTNode(unsigned char* strval, int base , int bit_width);