From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 31 Dec 2010 12:21:40 +0000 (+0000)
Subject: Extra assertion. Assert that internally created variables aren't already defined.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=47522012df3ce550d78c0e08a54a66a16ae28504;p=francis%2Fstp.git

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 734749f..197baca 100644
--- 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 50804f6..f6649fb 100644
--- 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);