diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-01 20:31:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-01 20:31:24 +0000 |
commit | 468c5bc5d8b63ec6818813270225e09383dd79ff (patch) | |
tree | adf53aa31607de77fd240b70b114a3396dfae4d8 /src/smt | |
parent | e0ea9a22721a332be2a2354846ffdf5f72c6a6de (diff) |
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
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
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(); |