From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 15 Apr 2016 21:54:15 +0000 (-0700)
Subject: Fix for bug 717
X-Git-Tag: cvc5-1.0.0~6049^2~66
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fff9135b57bed550b902af850ebb012fbe9ae6cd;p=cvc5.git

Fix for bug 717
---

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)