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.h6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e6029faef..e26ff51ef 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -68,7 +68,11 @@ class TheoryArith : public Theory {
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
-
+ /**
+ * Expand definition, which eliminates extended operators like div/mod in
+ * the given node.
+ */
+ TrustNode expandDefinition(Node node) override;
/**
* Does non-context dependent setup for a node connected to a theory.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback