diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-31 17:15:02 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-31 17:15:02 +0000 |
| commit | e0ea9a22721a332be2a2354846ffdf5f72c6a6de (patch) | |
| tree | 97f277ac1e6a203a3da3cfb5c41924bad86cc942 /src/smt | |
| parent | 48de3ac52d0fb8656b6e4e768c74be4be3b2a883 (diff) | |
Fixed bug in bv: one more case where non-shared equality was getting propagated
Added a global push and pop around solving - fixes an assertion failure when
TNodes are still around in a CDHashMap at destruction time.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0d3a220c9..64e3e4ae4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -293,6 +293,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->setDecisionEngine(d_decisionEngine); // d_decisionEngine->setPropEngine(d_propEngine); + d_context->push(); + d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); // [MGD 10/20/2011] keep around in incremental mode, due to a @@ -349,6 +351,8 @@ SmtEngine::~SmtEngine() throw() { shutdown(); + d_context->pop(); + if(d_assignments != NULL) { d_assignments->deleteSelf(); } |