fix errors in smt-lib2 output; needed for debugging

1 files changed, 17 insertions, 4 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0f5fcd73b..43649aa21 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -70,7 +70,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     switch(n.getKind()) {
     case kind::TYPE_CONSTANT:
       switch(n.getConst<TypeConstant>()) {
-      case BOOLEAN_TYPE: out << "Boolean"; break;
+      case BOOLEAN_TYPE: out << "Bool"; break;
       case REAL_TYPE: out << "Real"; break;
       case INTEGER_TYPE: out << "Int"; break;
       default:
@@ -103,7 +103,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::CONST_INTEGER: {
       Integer i = n.getConst<Integer>();
       if(i < 0) {
-        out << "(- " << i << ')';
+        out << "(- " << -i << ')';
       } else {
         out << i;
       }
@@ -112,12 +112,21 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::CONST_RATIONAL: {
       Rational r = n.getConst<Rational>();
       if(r < 0) {
-        out << "(- " << r << ')';
+        if(r.getDenominator() == 1) {
+          out << "(- " << -r << ')';
+        } else {
+          out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
+        }
       } else {
-        out << r;
+        if(r.getDenominator() == 1) {
+          out << r;
+        } else {
+          out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
+        }
       }
       break;
     }
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -163,6 +172,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::MINUS:
   case kind::UMINUS:
   case kind::DIVISION:
+  case kind::INTS_DIVISION:
+  case kind::INTS_MODULUS:
   case kind::LT:
   case kind::LEQ:
   case kind::GT:
@@ -275,6 +286,8 @@ static string smtKindString(Kind k) throw() {
   case kind::MINUS: return "-";
   case kind::UMINUS: return "-";
   case kind::DIVISION: return "/";
+  case kind::INTS_DIVISION: return "div";
+  case kind::INTS_MODULUS: return "mod";
   case kind::LT: return "<";
   case kind::LEQ: return "<=";
   case kind::GT: return ">";