Bugfix. Keep track of which symbols* have been deleted. Lots of them are duplicated...

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

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index c5de8e5cd8ef86b18ae8f74eebe6d55165c81aad..580005c6e06b245ef92908cc252025645fa334dd 100644 (file)
--- 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