diff options
Diffstat (limited to 'src/proof/theory_proof.cpp')
| -rw-r--r-- | src/proof/theory_proof.cpp | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 66109bfac..3103557c8 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1069,13 +1069,22 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; if (d_theory->getId()==theory::THEORY_UF) { - th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, + th = new theory::uf::TheoryUF(&fakeContext, + &fakeContext, + oc, + v, ProofManager::currentPM()->getLogicInfo(), + nullptr, "replay::"); } else if (d_theory->getId()==theory::THEORY_ARRAYS) { - th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, - ProofManager::currentPM()->getLogicInfo(), - "replay::"); + th = new theory::arrays::TheoryArrays( + &fakeContext, + &fakeContext, + oc, + v, + ProofManager::currentPM()->getLogicInfo(), + nullptr, + "replay::"); } else if (d_theory->getId() == theory::THEORY_ARITH) { Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl; os << " (clausify_false trust)"; |