diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-30 16:58:24 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-30 16:59:37 -0400 |
| commit | 7edd9eb6ecf8d36beea059a62ce573fdb6a6f8a1 (patch) | |
| tree | be1d5117c2801e1ca5c2d6d1db0cc562063855f7 /src/theory | |
| parent | a4a943134f888a514f19adaffe2f6743a16a25a6 (diff) | |
Proofs- and cores-related segfault fixes (mainly a usability issue), thanks Christoph Sticksel for reporting these.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 073f2ab94..01387637e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -65,6 +65,8 @@ using namespace CVC4; using namespace CVC4::theory; void TheoryEngine::finishInit() { + PROOF (ProofManager::initTheoryProof(); ); + // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); @@ -170,8 +172,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - PROOF (ProofManager::initTheoryProof(); ); - d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); StatisticsRegistry::registerStat(&d_arithSubstitutionsAdded); |