add a global user-context push/pop in smt engine, just like clark's addition the...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 64e3e4ae47ae6f1253c14101ae122874f542e71f..68485ca8ada98a267e58c3c0e6cd78d7e0f6e73c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -293,6 +293,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
   // d_decisionEngine->setPropEngine(d_propEngine);
 
+  // global push/pop around everything, to ensure proper destruction
+  // of context-dependent data structures
+  d_userContext->push();
   d_context->push();
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
@@ -345,13 +348,16 @@ SmtEngine::~SmtEngine() throw() {
   NodeManagerScope nms(d_nodeManager);
 
   try {
-    while(Options::current()->incrementalSolving && d_userContext->getLevel() > 0) {
+    while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
       internalPop();
     }
 
     shutdown();
 
+    // global push/pop around everything, to ensure proper destruction
+    // of context-dependent data structures
     d_context->pop();
+    d_userContext->pop();
 
     if(d_assignments != NULL) {
       d_assignments->deleteSelf();