2 files changed, 35 insertions, 17 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2d89d3aff..ed5116bc6 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -152,6 +152,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       case BOOLEAN_TYPE:
         out << "BOOLEAN";
         break;
+      case STRING_TYPE:
+        out << "STRING";
+        break;
       default:
         out << tc;
         break;
@@ -162,11 +165,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << n.getConst<Datatype>().getName();
       break;
 
-    case kind::EMPTYSET: {
+    case kind::EMPTYSET:
       out << "{} :: " << n.getConst<EmptySet>().getType();
-      return;
       break;
-    }
 
     case kind::STORE_ALL: {
       const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
@@ -176,8 +177,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     }
 
     default:
-      // fall back on whatever operator<< does on underlying type; we
-      // might luck out and print something reasonable
+      // Fall back to whatever operator<< does on underlying type; we
+      // might luck out and print something reasonable.
       kind::metakind::NodeValueConstPrinter::toStream(out, n);
     }
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cb1fe87b2..3ca5674e9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -245,7 +245,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   bool stillNeedToPrintParams = true;
   bool forceBinary = false; // force N-ary to binary when outputing children
   // operator
-  if(n.getNumChildren() != 0 && n.getKind()!=kind::INST_PATTERN_LIST) out << '(';
+  if(n.getNumChildren() != 0 &&
+     n.getKind() != kind::INST_PATTERN_LIST &&
+     n.getKind() != kind::APPLY_TYPE_ASCRIPTION) {
+    out << '(';
+  }
   switch(Kind k = n.getKind()) {
     // builtin theory
   case kind::APPLY: break;
@@ -307,7 +311,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STORE:
   case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
 
-  // string theory
+    // string theory
   case kind::STRING_CONCAT:
     if(d_variant == z3str_variant) {
       out << "Concat ";
@@ -425,12 +429,19 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
    // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
-      out << "as ";
-      toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
-      out << ' ';
       TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
-      out << (t.isFunctionLike() ? t.getRangeType() : t);
-      out << ')';
+      if(t.getKind() == kind::TYPE_CONSTANT &&
+         t.getConst<TypeConstant>() == REAL_TYPE &&
+         n[0].getType().isInteger()) {
+        // Special case, in model output integer constants that should be
+        // Real-sorted are wrapped in a type ascription.  Handle that here.
+        toStream(out, n[0], -1, false);
+        out << ".0";
+        return;
+      }
+      out << "(as ";
+      toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
+      out << ' ' << (t.isFunctionLike() ? t.getRangeType() : t) << ')';
       return;
     }
     break;
@@ -827,11 +838,11 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
     const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; 
     Node n = Node::fromExpr( dfc->getFunction() );
-    if(dfc->getPrintInModelSetByUser()){
-      if(!dfc->getPrintInModel()){
+    if(dfc->getPrintInModelSetByUser()) {
+      if(!dfc->getPrintInModel()) {
         return;
       }
-    }else if(n.getKind() == kind::SKOLEM) {
+    } else if(n.getKind() == kind::SKOLEM) {
       // don't print out internal stuff
       return;
     }
@@ -849,7 +860,13 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
         }
       }
       out << "(define-fun " << n << " () "
-          << n.getType() << " " << val << ")" << endl;
+          << n.getType() << " ";
+      if(val.getType().isInteger() && n.getType().isReal() && !n.getType().isInteger()) {
+        out << val << ".0";
+      } else {
+        out << val;
+      }
+      out << ")" << endl;
     }
 /*
     //for table format (work in progress)
@@ -874,7 +891,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       }
     }
 */
-  }else{
+  } else {
     out << c << endl;
   }
 }