From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 29 May 2013 13:48:40 +0000 (-0400)
Subject: SMT-LIB printer updates (some missing cases).
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7eba5fcb468399181d06a3684e760aae7185229;p=cvc5.git

SMT-LIB printer updates (some missing cases).
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c59df6269..b84d86a49 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -241,11 +241,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::MULT:
   case kind::MINUS:
   case kind::UMINUS:
-  case kind::DIVISION:
   case kind::LT:
   case kind::LEQ:
   case kind::GT:
-  case kind::GEQ: out << smtKindString(k) << " "; break;
+  case kind::GEQ:
+  case kind::DIVISION:
+  case kind::DIVISION_TOTAL:
+  case kind::INTS_DIVISION:
+  case kind::INTS_DIVISION_TOTAL:
+  case kind::INTS_MODULUS:
+  case kind::INTS_MODULUS_TOTAL: out << smtKindString(k) << " "; break;
 
     // arrays theory
   case kind::SELECT:
@@ -399,11 +404,16 @@ static string smtKindString(Kind k) throw() {
   case kind::MULT: return "*";
   case kind::MINUS: return "-";
   case kind::UMINUS: return "-";
-  case kind::DIVISION: return "/";
   case kind::LT: return "<";
   case kind::LEQ: return "<=";
   case kind::GT: return ">";
   case kind::GEQ: return ">=";
+  case kind::DIVISION:
+  case kind::DIVISION_TOTAL: return "/";
+  case kind::INTS_DIVISION:
+  case kind::INTS_DIVISION_TOTAL: return "div";
+  case kind::INTS_MODULUS:
+  case kind::INTS_MODULUS_TOTAL: return "mod";
 
     // arrays theory
   case kind::SELECT: return "select";