From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 28 May 2013 23:06:12 +0000 (-0400)
Subject: Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ebc6c79589ac7065d13f35e5997efdca869a5c58;p=cvc5.git

Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
---

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: