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 2310e73bd0f020dac1e0782159d06621ccc33f04..dd3836e8bb457750683bcf02697192af07ba58b7 100644 (file)
--- 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 ce86865ca0203a6e81f86922b87276af0fd3003e..750f542adbdc5c13ad0c5e234b10f342979c0624 100644 (file)
--- 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 24aefb8bcf4a9a726774f92bade21e46adcec07a..e13a72ae622fb929ea3555839e36f9cd85a55759 100644 (file)
--- 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);