diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-28 19:06:12 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-29 10:07:26 -0400 |
| commit | ebc6c79589ac7065d13f35e5997efdca869a5c58 (patch) | |
| tree | eb278f19943150aab405c0da83278436743d2c91 /src/parser | |
| parent | 735bf7daa07b016aa7964cabdcef27a918d4a96a (diff) | |
Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
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: |