Partial fix for bug 435; still needs some effort.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 11 insertions, 3 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a61d2d4c0..a9d439a0f 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -290,6 +290,17 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     // DATATYPES
+    case kind::PARAMETRIC_DATATYPE:
+      out << n[0].getConst<Datatype>().getName() << '[';
+      for(unsigned i = 1; i < n.getNumChildren(); ++i) {
+        if(i > 1) {
+          out << ',';
+        }
+        out << n[i];
+      }
+      out << ']';
+      return;
+      break;
     case kind::APPLY_TYPE_ASCRIPTION: {
         toStream(out, n[0], depth, types, false);
         out << "::";
@@ -462,9 +473,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << ">=";
       opType = INFIX;
       break;
-    case kind::PARAMETRIC_DATATYPE:
-      out << n[0].getConst<Datatype>().getName();
-      break;
 
     // BITVECTORS
     case kind::BITVECTOR_XOR: