diff options
Diffstat (limited to 'src/proof/uf_proof.cpp')
| -rw-r--r-- | src/proof/uf_proof.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index b88f7dc33..9e5b82232 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -581,8 +581,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, } } -UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe) - : TheoryProof(uf, pe) +UFProof::UFProof(Environment* env, + theory::uf::TheoryUF* uf, + TheoryProofEngine* pe) + : TheoryProof(env, uf, pe) {} theory::TheoryId UFProof::getTheoryId() { return theory::THEORY_UF; } @@ -626,7 +628,7 @@ void UFProof::registerTerm(Expr term) { void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; - Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF); + Assert(d_env->theoryOf(term) == theory::THEORY_UF); if (term.getKind() == kind::VARIABLE || term.getKind() == kind::SKOLEM || |