diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2016-04-15 14:54:15 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-04-15 14:54:15 -0700 |
| commit | fff9135b57bed550b902af850ebb012fbe9ae6cd (patch) | |
| tree | d3ef29153f087292fc1c2583a8c3175d342fce6f /src | |
| parent | 5ae7ee3df2cc0bd5644a0391bb22be291fb65abc (diff) | |
Fix for bug 717
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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) |