diff options
| author | Guy <katz911@gmail.com> | 2016-06-20 05:40:20 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-06-20 05:40:20 -0700 |
| commit | 150863561376c8cb7b170793f693352eab582ba9 (patch) | |
| tree | c324dc74f248573b19096cea862534430e22b1f8 | |
| parent | f948414b8b9979f3e680abdedf8e3e6fbbbdd226 (diff) | |
Fixed a bug where the proofManager's init() call was not getting called, resutling a null point deference
| -rw-r--r-- | src/proof/proof_manager.cpp | 8 | ||||
| -rw-r--r-- | src/smt/smt_engine_scope.h | 1 | ||||
| -rw-r--r-- | 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<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()); |