Fix for bug 717

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 771195a381d8410538b3e592339641e4eebbe564..5bd1cbdfc599ef2aba1fab6a5774a86cfe647c79 100644 (file)
--- 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)