From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 30 Jun 2015 04:16:47 +0000 (-0400)
Subject: fix smt2 parameterized sort printing
X-Git-Tag: cvc5-1.0.0~6267^2~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=841c33c4b0b22c73951634fa6df5bf1b7065adbf;p=cvc5.git

fix smt2 parameterized sort printing
---

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;