summaryrefslogtreecommitdiff
path: root/src/theory/arith/congruence_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/congruence_manager.h')
-rw-r--r--src/theory/arith/congruence_manager.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 18ecbeb9d..5e4616628 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -56,7 +56,7 @@ private:
Unreachable();
}
- bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_acm.propagate(t1.eqNode(t2));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback