From: Guy <katz911@gmail.com>
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<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
-  PROOF (ProofManager::currentPM()->initTheoryProofEngine(); );
+#ifdef CVC4_PROOF
+  ProofManager::currentPM()->initTheoryProofEngine();
+#endif
 
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());