fix smt2 parameterized sort printing

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 79cb18d92c472574a251473e8be05b32cfaf940d..5cc04427221dedfa55e0297350d82b7564374cbf 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -288,10 +288,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
   if(n.getKind() == kind::SORT_TYPE) {
     string name;
+    if(n.getNumChildren() != 0) {
+      out << '(';
+    }
     if(n.getAttribute(expr::VarNameAttr(), name)) {
       out << maybeQuoteSymbol(name);
-      return;
     }
+    if(n.getNumChildren() != 0) {
+      for(unsigned i = 0; i < n.getNumChildren(); ++i) {
+       out << ' ';
+       toStream(out, n[i], toDepth, types);
+      }
+      out << ')';
+    }
+    return;
   }
 
   bool stillNeedToPrintParams = true;