This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.

1 files changed, 1 insertions, 6 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 857513fa3..1f147479d 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -94,18 +94,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::CONST_RATIONAL: {
       const Rational& rat = n.getConst<Rational>();
-      if(rat.getDenominator() == 1) {
+      if(rat.isIntegral()) {
         out << rat.getNumerator();
       } else {
         out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
       }
       break;
     }
-    case kind::CONST_INTEGER: {
-      const Integer& num = n.getConst<Integer>();
-      out << num;
-      break;
-    }
     case kind::CONST_PSEUDOBOOLEAN: {
       const Pseudoboolean& num = n.getConst<Pseudoboolean>();
       out << num;