Mostly resolves bug #561 memory leaks, and more.

1 files changed, 10 insertions, 5 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index e5705882a..c8a08dad9 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,10 +31,15 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
 
 }
 
+InstantiationEngine::~InstantiationEngine() {
+  delete d_i_ag;
+  delete d_isup;
+}
+
 void InstantiationEngine::finishInit(){
   //for UF terms
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
@@ -48,14 +53,14 @@ void InstantiationEngine::finishInit(){
     }else{
       d_isup = NULL;
     }
-    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 );
-    i_ag->setGenerateAdditional( true );
-    addInstStrategy( i_ag );
+    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 );
+    d_i_ag->setGenerateAdditional( true );
+    addInstStrategy( d_i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
     if( !options::finiteModelFind() && options::fullSaturateQuant() ){
       addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
     }
-    //d_isup->setPriorityOver( i_ag );
+    //d_isup->setPriorityOver( d_i_ag );
     //d_isup->setPriorityOver( i_agm );
     //i_ag->setPriorityOver( i_agm );
   }