summaryrefslogtreecommitdiff
path: root/src/proof/arith_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/arith_proof.cpp')
-rw-r--r--src/proof/arith_proof.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 3b57be1f2..1d51f99e1 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -640,8 +640,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
}
ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe)
- : TheoryProof(arith, pe), d_realMode(false)
-{}
+ : TheoryProof(arith, pe), d_recorder(), d_realMode(false)
+{
+ arith->setProofRecorder(&d_recorder);
+}
theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; }
void ArithProof::registerTerm(Expr term) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback