From 1af684a72f31f54243eca9ef902c0e7ecd8486d7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 24 Mar 2016 10:44:05 -0700 Subject: Fixing a memory leak in QuantInfo::d_var_mg. --- src/theory/quantifiers/rewrite_engine.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/rewrite_engine.cpp') diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 4c8050239..a8cdd2bc2 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -124,12 +124,13 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f ); if( it!=d_qinfo.end() ){ QuantInfo * qi = &it->second; - if( qi->d_mg->isValid() ){ + if( qi->matchGeneratorIsValid() ){ Node rr = TermDb::getRewriteRule( f ); Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; qi->reset_round( qcf ); Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - while( qi->d_mg->getNextMatch( qcf, qi ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ + while( qi->getNextMatch( qcf ) && + ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl; qi->debugPrintMatch( "rewrite-engine-inst-debug" ); std::vector< int > assigned; -- cgit v1.2.3