Extra assertion. Assert that internally created variables aren't already defined.

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 734749f554c1623d100558c1a7560132c2d5cec0..197bacaec8f78d7af666ffeadf479f6438e5ed7e 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -147,6 +147,19 @@ namespace BEEV
       return true;
   }
 
+  bool STPMgr::LookupSymbol(const char * const name)
+  {
+    ASTSymbol s(name);
+    ASTSymbol* s_ptr = &s; // it's a temporary key.
+
+    if (_symbol_unique_table.find(s_ptr) ==
+        _symbol_unique_table.end())
+      return false;
+    else
+      return true;
+  }
+
+
   //Create a ASTBVConst node
   ASTNode STPMgr::CreateBVConst(unsigned int width, 
                                unsigned long long int bvconst)

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 50804f68222ab341412e916a124956a22eec7a1b..f6649fba2e36b83b12a093a73b88dd93759f2a41 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -139,6 +139,8 @@ namespace BEEV
     CBV CreateBVConstVal;
 
   public:
+
+    bool LookupSymbol(const char * const name);
     
     /****************************************************************
      * Public Flags                                                 *
@@ -395,6 +397,7 @@ namespace BEEV
     {
         char d[32 + prefix.length()];
         sprintf(d, "%s_%d", prefix.c_str(), _symbol_count++);
+        assert(!LookupSymbol(d));
 
         BEEV::ASTNode CurrentSymbol = CreateSymbol(d,indexWidth,valueWidth);
         Introduced_SymbolsSet.insert(CurrentSymbol);