diff options
| -rw-r--r-- | src/proof/resolution_bitvector_proof.h | 3 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 21 |
2 files changed, 14 insertions, 10 deletions
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index a54d72d3f..ccb288f6e 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -98,6 +98,8 @@ class ResolutionBitVectorProof : public BitVectorProof void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override; protected: + context::Context d_fakeContext; + // The CNF formula that results from bit-blasting will need a proof. // This is that proof. std::unique_ptr<BVSatProof> d_resolutionProof; @@ -105,7 +107,6 @@ class ResolutionBitVectorProof : public BitVectorProof bool d_isAssumptionConflict; theory::TheoryId getTheoryId() override; - context::Context d_fakeContext; }; class LFSCBitVectorProof : public ResolutionBitVectorProof 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; |