From fff9135b57bed550b902af850ebb012fbe9ae6cd Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 15 Apr 2016 14:54:15 -0700 Subject: [PATCH] Fix for bug 717 --- src/smt/smt_engine.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 771195a38..5bd1cbdfc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1063,7 +1063,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are // initialized in TheoryEngine and PropEngine respectively. Assert(d_proofManager == NULL); - PROOF( d_proofManager = new ProofManager(); ); +#ifdef CVC4_PROOF + d_proofManager = new ProofManager(); +#endif // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) -- 2.30.2