From 468c5bc5d8b63ec6818813270225e09383dd79ff Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 1 Jun 2012 20:31:24 +0000 Subject: [PATCH] add a global user-context push/pop in smt engine, just like clark's addition the other day of a push/pop of the sat context --- src/smt/smt_engine.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 64e3e4ae4..68485ca8a 100644 --- 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(); -- 2.30.2