summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r--src/theory/arith/theory_arith.h5
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 9381b7341..30de7bbad 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -99,10 +99,7 @@ class TheoryArith : public Theory {
Node getModelValue(TNode var) override;
- std::pair<bool, Node> entailmentCheck(
- TNode lit,
- const EntailmentCheckParameters* params,
- EntailmentCheckSideEffects* out) override;
+ std::pair<bool, Node> entailmentCheck(TNode lit) override;
void setProofRecorder(proof::ArithProofRecorder* proofRecorder)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback