From: Guy Date: Mon, 20 Jun 2016 12:40:20 +0000 (-0700) Subject: Fixed a bug where the proofManager's init() call was not getting called, resutling... X-Git-Tag: cvc5-1.0.0~6049^2~7 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=150863561376c8cb7b170793f693352eab582ba9;p=cvc5.git Fixed a bug where the proofManager's init() call was not getting called, resutling a null point deference --- 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());