From 2ef8f732e7a51621a4fd455220a7120898dab534 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Jun 2010 14:07:25 +0000
Subject: [PATCH] Bugfix. Keep track of which symbols* have been deleted. Lots
 of them are duplicated in the map.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@867 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.h | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index c5de8e5..580005c 100644
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -158,17 +158,27 @@ namespace BEEV
     }
     ;
 
+	  void ClearAllCaches()
+	  {
+	  TermsAlreadySeenMap.clear();
+	  DoNotSolve_TheseVars.clear();
+	  FormulasAlreadySolvedMap.clear();
+	  //TermsAlreadySeenMap_ForArrays.clear();
+	  set<Symbols*> deleted;
+	  for (ASTNodeToNodes::iterator it = symbol_graph.begin(); it != symbol_graph.end(); it++)
+	  {
+		  if (deleted.find(it->second) == deleted.end())
+		  {
+			  deleted.insert(it->second);
+			  delete it->second;
+		  }
+	  }
+	  }
+
     //Destructor
     ~BVSolver()
       {
-        TermsAlreadySeenMap.clear();
-        DoNotSolve_TheseVars.clear();
-        FormulasAlreadySolvedMap.clear();
-        //TermsAlreadySeenMap_ForArrays.clear();
-        for (ASTNodeToNodes::iterator it = symbol_graph.begin(); it != symbol_graph.end(); it++)
-         {
-            	delete it->second;
-        }
+    	ClearAllCaches();
       }
 
     //Top Level Solver: Goes over the input DAG, identifies the
-- 
2.47.3