Fix subgoal generation context (#1816)

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;