diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-10 14:45:36 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-10 14:45:36 -0700 |
commit | b7d0c09bd12b9d0f46deab199714ce3441206d7f (patch) | |
tree | c894889a35ce3f5b446e9d160af88e74aeb4c63e /src/theory/quantifiers_engine.cpp | |
parent | 8c860213ca3a43e1fe483accb4b2b928ae14028e (diff) |
Fix memory leak in quantifiers engine (#1219)
Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak
where d_quant_attr was not deleted when the QuantifiersEngine was
destroyed. This commit fixes the issue by turning d_quant_attr into an
std::unique_ptr.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0e10dfe54..b0f548625 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -61,22 +61,24 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): - d_te( te ), - d_conflict_c(c, false), - //d_quants(u), - d_quants_red(u), - d_lemmas_produced_c(u), - d_skolemized(u), - d_ierCounter_c(c), - //d_ierCounter(c), - //d_ierCounter_lc(c), - //d_ierCounterLastLc(c), - d_presolve(u, true), - d_presolve_in(u), - d_presolve_cache(u), - d_presolve_cache_wq(u), - d_presolve_cache_wic(u){ +QuantifiersEngine::QuantifiersEngine(context::Context* c, + context::UserContext* u, TheoryEngine* te) + : d_te(te), + d_conflict_c(c, false), + // d_quants(u), + d_quants_red(u), + d_lemmas_produced_c(u), + d_skolemized(u), + d_quant_attr(new quantifiers::QuantAttributes(this)), + d_ierCounter_c(c), + // d_ierCounter(c), + // d_ierCounter_lc(c), + // d_ierCounterLastLc(c), + d_presolve(u, true), + d_presolve_in(u), + d_presolve_cache(u), + d_presolve_cache_wq(u), + d_presolve_cache_wic(u) { //utilities d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this ); d_util.push_back( d_eq_query ); @@ -91,8 +93,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* }else{ d_sygus_tdb = NULL; } - - d_quant_attr = new quantifiers::QuantAttributes( this ); if( options::instPropagate() ){ // notice that this option is incompatible with options::qcfAllConflict() |