From 150863561376c8cb7b170793f693352eab582ba9 Mon Sep 17 00:00:00 2001 From: Guy Date: Mon, 20 Jun 2016 05:40:20 -0700 Subject: [PATCH] Fixed a bug where the proofManager's init() call was not getting called, resutling a null point deference --- src/proof/proof_manager.cpp | 8 ++++---- src/smt/smt_engine_scope.h | 1 - src/theory/theory_engine.cpp | 4 +++- 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 65a6b1950..45b1f046e 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -62,10 +62,10 @@ ProofManager::ProofManager(ProofFormat format): } ProofManager::~ProofManager() { - delete d_satProof; - delete d_cnfProof; - delete d_theoryProof; - delete d_fullProof; + if (d_satProof) delete d_satProof; + if (d_cnfProof) delete d_cnfProof; + if (d_theoryProof) delete d_theoryProof; + if (d_fullProof) delete d_fullProof; } ProofManager* ProofManager::currentPM() { diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index e00be40d4..9407ff498 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -49,7 +49,6 @@ inline bool smtEngineInScope() { // FIXME: Maybe move into SmtScope? inline ProofManager* currentProofManager() { #if IS_PROOFS_BUILD - Assert(options::proof() || options::unsatCores()); Assert(s_smtEngine_current != NULL); return s_smtEngine_current->d_proofManager; #else /* IS_PROOFS_BUILD */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 618fda4c0..34eff5a47 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -261,7 +261,9 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - PROOF (ProofManager::currentPM()->initTheoryProofEngine(); ); +#ifdef CVC4_PROOF + ProofManager::currentPM()->initTheoryProofEngine(); +#endif d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); -- 2.30.2