From c6d487909fc799140519c435bae740860a660366 Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Thu, 24 Mar 2016 11:21:31 -0700
Subject: [PATCH] Fixing a memory leak in CDInstMatchTrie::d_data.

---
 src/theory/quantifiers/inst_match.cpp | 10 ++++++++++
 src/theory/quantifiers/inst_match.h   | 10 +++++-----
 2 files changed, 15 insertions(+), 5 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 );
     }
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 35353863c..7db59e88b 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -96,7 +96,7 @@ public:
   public:
     std::vector< int > d_order;
   };/* class InstMatchTrie ImtIndexOrder */
-public:
+
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
 private:
@@ -141,18 +141,18 @@ public:
 
 /** trie for InstMatch objects */
 class CDInstMatchTrie {
-public:
+private:
   /** the data */
   std::map< Node, CDInstMatchTrie* > d_data;
   /** is valid */
   context::CDO< bool > d_valid;
-private:
+
   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
-  ~CDInstMatchTrie(){}
-public:
+  ~CDInstMatchTrie();
+
   /** return true if m exists in this trie
         modEq is if we check modulo equality
         modInst is if we return true if m is an instance of a match that exists
-- 
2.30.2