From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 5 Dec 2013 17:54:40 +0000 (-0500)
Subject: Fixes related to parametric datatype printing.
X-Git-Tag: cvc5-1.0.0~7200
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2fab0a67761f8b63a3c3f5abdbe7f382f722a04f;p=cvc5.git

Fixes related to parametric datatype printing.
---

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