Fixed a serious memory error in vc_Destroy(). Deleting the STPMgr independent of...

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

diff --git a/src/AST/ASTSymbol.cpp b/src/AST/ASTSymbol.cpp
index c6540f496abba03854db84b180b4e9465d3276bb..6e1ea6d64eb3a0acb8504e9d90a66bb92122be5b 100644 (file)
--- a/src/AST/ASTSymbol.cpp
+++ b/src/AST/ASTSymbol.cpp
@@ -37,17 +37,17 @@ namespace BEEV
     delete this;
   }//End of cleanup()
 
-  unsigned long hash(unsigned char *str)
+  unsigned long long hash(unsigned char *str)
   {
-    unsigned long hash = 5381;
-    int c;
+    unsigned long long hash = 5381;
+    long long c;
     
     while (c = *str++)
       hash = ((hash << 5) + hash) + c; /* hash * 33 + c */
 
     //cout << "Hash value computed is: " << hash << endl;
     
-    return hash;
+    return (unsigned long long)hash;
   }
 
 

diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h
index e779c619a6280e02984eb15825a068c45d531dca..c30b5581ed7626f00005ab565999b64bd67487c3 100644 (file)
--- a/src/AST/ASTSymbol.h
+++ b/src/AST/ASTSymbol.h
@@ -12,7 +12,7 @@
 
 namespace BEEV
 {
-  unsigned long hash(unsigned char *str);
+  unsigned long long hash(unsigned char *str);
 
   /******************************************************************
    *  Class ASTSymbol:                                              *

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index efd58b0c329bff09c8b212ee5fef3183582b935e..4c9899dc4c7a40eb311fc00f81a25006c0bb6f7d 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -89,12 +89,12 @@ namespace BEEV
     
     void ClearAllTables(void)
     {
-      bm->ClearAllTables();
       simp->ClearAllTables();
       bvsolver->ClearAllTables();
       arrayTransformer->ClearAllTables();
       tosat->ClearAllTables();
       Ctr_Example->ClearAllTables();
+      bm->ClearAllTables();
     }
   }; //End of Class STP
 };//end of namespace

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 8125219aaac636f16d7bea40fcb8b29cdbb45957..478068fd18634926e76546711d2c566e0a820b1d 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -370,15 +370,17 @@ namespace BEEV
 
     void ClearAllTables(void) 
     {
-      // _interior_unique_table.clear();
-      // _bvconst_unique_table.clear();
-      // _symbol_unique_table.clear();
       NodeLetVarMap.clear();
       NodeLetVarMap1.clear();
       PLPrintNodeSet.clear();
       AlreadyPrintedSet.clear();
       StatInfoSet.clear();
-      //_asserts.clear();
+      
+      //DO NOT UNCOMMENT
+      //   _asserts.clear();
+      //   _interior_unique_table.clear();
+      //   _bvconst_unique_table.clear();
+      //   _symbol_unique_table.clear();      
     } //End of ClearAllTables()
 
   };//End of Class STPMgr

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 3e816c8cdfe0f57fac444d66bde52aca382f234a..fdfea2101f32a51451d106dc40030d389e693dba 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1718,7 +1718,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
     BEEV::FatalError("");
   }
 
-  //BEEV::GlobalSTP = (stpstar)vc;
+  BEEV::GlobalSTP = (stpstar)vc;
   CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
   if(0 != c) {
     cout << CONSTANTBV::BitVector_Error(c) << endl;
@@ -1729,7 +1729,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
   cvcparse((void*)AssertsQuery);
   BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
   BEEV::ASTNode query   = (*(BEEV::ASTVec*)AssertsQuery)[1];
-  //BEEV::GlobalSTP->TopLevelSTP(asserts, query);
+  BEEV::GlobalSTP->TopLevelSTP(asserts, query);
 
   node oo = b->CreateNode(BEEV::NOT,query);
   node o = b->CreateNode(BEEV::AND,asserts,oo);
@@ -1836,7 +1836,7 @@ void vc_Destroy(VC vc) {
   //     delete aaa;
   //   }
   delete decls;
-  delete b;
+  delete (stpstar)vc;
 }
 
 void vc_DeleteExpr(Expr e) {

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index d1da6233f702b8fe05efb524e105869748b9a75f..5880fce68b6a7a2505a9ceee1bd436da0de045d3 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -1,4 +1,5 @@
-CXXFLAGS=-DEXT_HASH_MAP -m32 -I../../src/c_interface -L../../lib
+include ../../scripts/Makefile.common
+CXXFLAGS=-DEXT_HASH_MAP $(CFLAGS) $(CFLAGS_M32) -I../../src/c_interface -L../../lib
 
 
 all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19