Fixes related to parametric datatype printing.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 869e02326d871b6e35617fceea11b7dec7945e3c..cac5eb266becbf8683fc37c12a3f474a410644c7 100644 (file)
--- 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