diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a0939f4db..6814ad531 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1071,6 +1071,18 @@ SmtEngine::~SmtEngine() //destroy all passes before destroying things that they refer to d_private->cleanupPreprocessingPasses(); + // d_proofManager is always created when proofs are enabled at configure + // time. Because of this, this code should not be wrapped in PROOF() which + // additionally checks flags such as options::proof(). + // + // Note: the proof manager must be destroyed before the theory engine. + // Because the destruction of the proofs depends on contexts owned be the + // theory solvers. +#ifdef CVC4_PROOF + delete d_proofManager; + d_proofManager = NULL; +#endif + delete d_theoryEngine; d_theoryEngine = NULL; delete d_propEngine; @@ -1078,15 +1090,6 @@ SmtEngine::~SmtEngine() delete d_decisionEngine; d_decisionEngine = NULL; - -// d_proofManager is always created when proofs are enabled at configure time. -// Becuase of this, this code should not be wrapped in PROOF() which -// additionally checks flags such as options::proof(). -#ifdef CVC4_PROOF - delete d_proofManager; - d_proofManager = NULL; -#endif - delete d_stats; d_stats = NULL; delete d_statisticsRegistry; |