Fixing a memory leak in CDInstMatchTrie::d_data.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index ead2bc57c..f204fed4b 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -225,6 +225,15 @@ void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::
   }
 }
 
+CDInstMatchTrie::~CDInstMatchTrie() {
+  for(std::map< Node, CDInstMatchTrie* >::iterator i = d_data.begin(),
+          iend = d_data.end(); i != iend; ++i) {
+    CDInstMatchTrie* current = (*i).second;
+    delete current;
+  }
+  d_data.clear();
+}
+
 
 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
                                     context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
@@ -285,6 +294,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
     if( !onlyExist ){
       // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
       CDInstMatchTrie* imt = new CDInstMatchTrie( c );
+      Assert(d_data.find(n) == d_data.end());
       d_data[n] = imt;
       imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
     }