From 68a994dbb7527b6f98975bbb776687413f23d451 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 26 Apr 2018 11:59:58 -0500
Subject: [PATCH] Fix subgoal generation context (#1816)

---
 .../quantifiers/conjecture_generator.cpp      | 25 ++++++++++++++-----
 src/theory/quantifiers/conjecture_generator.h |  1 +
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 142f9beae..404f64471 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -95,6 +95,19 @@ d_ee_conjectures( c ){
 
 }
 
+ConjectureGenerator::~ConjectureGenerator()
+{
+  for (std::map<Node, EqcInfo*>::iterator i = d_eqc_info.begin(),
+                                          iend = d_eqc_info.end();
+       i != iend;
+       ++i)
+  {
+    EqcInfo* current = (*i).second;
+    Assert(current != nullptr);
+    delete current;
+  }
+}
+
 void ConjectureGenerator::eqNotifyNewClass( TNode t ){
   Trace("thm-ee-debug") << "UEE : new equivalence class " << t << std::endl;
   d_upendingAdds.push_back( t );
@@ -1470,6 +1483,9 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
           d_status_child_num++;
           return getNextTerm( s, depth );
         }else{
+          Trace("sg-gen-tg-debug2")
+              << "...remove child from context " << std::endl;
+          s->changeContext(false);
           d_children.pop_back();
           d_status_child_num--;
           return getNextTerm( s, depth );
@@ -1492,11 +1508,7 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
     d_status_num = -1;
     return getNextTerm( s, depth );
   }else{
-    //clean up
     Assert( d_children.empty() );
-    Trace("sg-gen-tg-debug2") << "...remove from context " << this << std::endl;
-    s->changeContext( false );
-    Assert( d_id==s->d_tg_id );
     return false;
   }
 }
@@ -1815,9 +1827,10 @@ bool TermGenEnv::getNextTerm() {
     }else{
       return true;
     }
-  }else{
-    return false;
   }
+  Trace("sg-gen-tg-debug2") << "...remove from context " << std::endl;
+  changeContext(false);
+  return false;
 }
 
 //reset matching
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 764379e76..2db175fae 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -420,6 +420,7 @@ private:  //information about ground equivalence classes
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 public:
   ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
+  ~ConjectureGenerator();
 
   /* needs check */
   bool needsCheck(Theory::Effort e) override;
-- 
2.30.2