diff options
author | Tim King <taking@google.com> | 2016-03-22 21:22:15 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-03-22 21:22:15 -0700 |
commit | b3fa70606f42944044c5ed08f66904b8bdb064b1 (patch) | |
tree | affcdc52744b9a335a77c480fc2c105df34c287b /src | |
parent | c91733f4b458cb888d915baa309b2ba29488fa10 (diff) |
Deleting the CDInstMatchTries in QuantifiersEngine::d_c_inst_match_trie.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 754b0c224..1aeb6f517 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -151,6 +151,14 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* } QuantifiersEngine::~QuantifiersEngine(){ + for(std::map< Node, inst::CDInstMatchTrie* >::iterator + i = d_c_inst_match_trie.begin(), iend = d_c_inst_match_trie.end(); + i != iend; ++i) + { + delete (*i).second; + } + d_c_inst_match_trie.clear(); + delete d_alpha_equiv; delete d_builder; delete d_rr_engine; |