diff options
Diffstat (limited to 'src/proof/theory_proof.cpp')
| -rw-r--r-- | src/proof/theory_proof.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index b0d6988a5..1bc8ae949 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -111,10 +111,9 @@ public: void done(TNode node) { } }; /* class MyPreRegisterVisitor */ -TheoryProofEngine::TheoryProofEngine(SmtGlobals* globals) +TheoryProofEngine::TheoryProofEngine() : d_registrationCache() , d_theoryProofTable() - , d_globals(globals) { d_theoryProofTable[theory::THEORY_BOOL] = new LFSCBooleanProof(this); } @@ -508,12 +507,10 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& if(d_theory->getId()==theory::THEORY_UF) { th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), - ProofManager::currentPM()->getTheoryProofEngine()->d_globals, "replay::"); } else if(d_theory->getId()==theory::THEORY_ARRAY) { th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), - ProofManager::currentPM()->getTheoryProofEngine()->d_globals, "replay::"); } else { InternalError(std::string("can't generate theory-proof for ") + ProofManager::currentPM()->getLogic()); |