diff options
author | Tim King <taking@google.com> | 2016-03-24 11:21:31 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-03-24 11:21:31 -0700 |
commit | c6d487909fc799140519c435bae740860a660366 (patch) | |
tree | 655ecafc71039c1e6e7ab711f0933fad4413a62c /src/theory/quantifiers/inst_match.cpp | |
parent | 5b8ced2895439fd9612bc3bf2485056f41219d03 (diff) |
Fixing a memory leak in CDInstMatchTrie::d_data.
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 10 |
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 ); } |