From 2fab0a67761f8b63a3c3f5abdbe7f382f722a04f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 5 Dec 2013 12:54:40 -0500
Subject: [PATCH] Fixes related to parametric datatype printing.

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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 869e02326..cac5eb266 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -326,12 +326,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       out << ' ';
       TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
       out << (t.isFunctionLike() ? t.getRangeType() : t);
-      stillNeedToPrintParams = false;
+      out << ')';
+      return;
     }
     break;
   case kind::APPLY_TESTER:
   case kind::APPLY_CONSTRUCTOR:
   case kind::APPLY_SELECTOR:
+  case kind::PARAMETRIC_DATATYPE:
     break;
 
     // quantifiers
-- 
2.30.2