From 841c33c4b0b22c73951634fa6df5bf1b7065adbf Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 30 Jun 2015 00:16:47 -0400
Subject: [PATCH] fix smt2 parameterized sort printing

---
 src/printer/smt2/smt2_printer.cpp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 79cb18d92..5cc044272 100644
--- 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;
-- 
2.30.2