Mostly resolves bug #561 memory leaks, and more.

1 files changed, 4 insertions, 1 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 394d53d42..53777d362 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -25,6 +25,7 @@ namespace theory {
 namespace quantifiers {
 
 class InstStrategyUserPatterns;
+class InstStrategyAutoGenTriggers;
 
 /** instantiation strategy class */
 class InstStrategy {
@@ -79,6 +80,8 @@ private:
   std::map< InstStrategy*, bool > d_instStrategyActive;
   /** user-pattern instantiation strategy */
   InstStrategyUserPatterns* d_isup;
+  /** auto gen triggers; only kept for destructor cleanup */
+  InstStrategyAutoGenTriggers* d_i_ag;
   /** is instantiation strategy active */
   bool isActiveStrategy( InstStrategy* is ) {
     return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
@@ -123,7 +126,7 @@ private:
   void debugSat( int reason );
 public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
-  ~InstantiationEngine(){}
+  ~InstantiationEngine();
   /** initialize */
   void finishInit();