summaryrefslogtreecommitdiff
path: root/src/proof/arith_proof.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/arith_proof.h')
-rw-r--r--src/proof/arith_proof.h7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index c70754a1f..ac96ad1f3 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -82,9 +82,10 @@ public:
LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
: ArithProof(arith, proofEngine)
{}
- void printOwnedTerm(Expr term,
- std::ostream& os,
- const ProofLetMap& map) override;
+ void printOwnedTermAsType(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map,
+ TypeNode expectedType) override;
void printOwnedSort(Type type, std::ostream& os) override;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback