diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a4623bdfc..c042c3992 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -36,7 +36,6 @@ void Smt2::addArithmeticOperators() { addOperator(kind::MINUS); addOperator(kind::UMINUS); addOperator(kind::MULT); - addOperator(kind::DIVISION); addOperator(kind::LT); addOperator(kind::LEQ); addOperator(kind::GT); @@ -106,16 +105,20 @@ void Smt2::addTheory(Theory theory) { case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); - // falling-through on purpose, to add Ints part of RealsInts + addOperator(kind::DIVISION); + // falling through on purpose, to add Ints part of Reals_Ints case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); + addOperator(kind::INTS_DIVISION); + addOperator(kind::INTS_MODULUS); break; case THEORY_REALS: defineType("Real", getExprManager()->realType()); addArithmeticOperators(); + addOperator(kind::DIVISION); break; case THEORY_BITVECTORS: |