Fixed a bug where the proofManager's init() call was not getting called, resutling...

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 65a6b1950f16067e5886dda23b613102c43e2a22..45b1f046eeec595e34666f7d7d8dfa8e403e0495 100644 (file)
--- 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 e00be40d49d918141dae90f380b084f721648687..9407ff4983e826213f309290e63bdfab018e07c8 100644 (file)
--- 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 618fda4c0e17c5e80a64b33b7ef2fa8738ef33d2..34eff5a478190d38f7289d419ed8a40569233476 100644 (file)
--- 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());