summaryrefslogtreecommitdiff
path: root/src/theory/arith/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/kinds')
-rw-r--r--src/theory/arith/kinds1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index fafa33a68..99f7258da 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -10,6 +10,7 @@ operator PLUS 2: "arithmetic addition"
operator MULT 2: "arithmetic multiplication"
operator MINUS 2 "arithmetic binary subtraction operator"
operator UMINUS 1 "arithmetic unary negation"
+operator DIVISION 2 "arithmetic division"
constant CONST_RATIONAL \
::CVC4::Rational \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback