summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2015-04-15 23:34:37 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2015-04-15 23:34:37 -0400
commit5c64edb7e3228b366b6c51e4dfd2a3dd350f9e2c (patch)
tree127abd63e7e4b769fe843e7064d279463265d74a /src/parser/smt2/smt2.cpp
parent7d00e71793a0af9b5eef1951ed3208863db90855 (diff)
THEORY_INTS parser changes
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r--src/parser/smt2/smt2.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 73a5124e0..85f2d1ec5 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -168,9 +168,9 @@ void Smt2::addTheory(Theory theory) {
case THEORY_INTS:
defineType("Int", getExprManager()->integerType());
addArithmeticOperators();
- Parser::addOperator(kind::INTS_DIVISION);
- Parser::addOperator(kind::INTS_MODULUS);
- Parser::addOperator(kind::ABS);
+ addOperator(kind::INTS_DIVISION, "div");
+ addOperator(kind::INTS_MODULUS, "mod");
+ addOperator(kind::ABS, "abs");
Parser::addOperator(kind::DIVISIBLE);
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback