From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Jun 2021 21:16:40 +0000 (-0500)
Subject: Fixes for printing define-fun-rec (#6673)
X-Git-Tag: cvc5-1.0.0~1651
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87b204084e86b534571f16250ca4871150b2a783;p=cvc5.git

Fixes for printing define-fun-rec (#6673)
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4607d2747..04a57e0e9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1698,21 +1698,20 @@ void Smt2Printer::toStreamCmdDefineFunctionRec(
     out << funcs[i] << " (";
     // print its type signature
     vector<Node>::const_iterator itf = formals[i].cbegin();
-    for (;;)
+    while (itf != formals[i].cend())
     {
       out << "(" << (*itf) << " " << (*itf).getType() << ")";
       ++itf;
-      if (itf != formals[i].end())
+      if (itf != formals[i].cend())
       {
         out << " ";
       }
-      else
-      {
-        break;
-      }
     }
     TypeNode type = funcs[i].getType();
-    type = type.getRangeType();
+    if (type.isFunction())
+    {
+      type = type.getRangeType();
+    }
     out << ") " << type;
     if (funcs.size() > 1)
     {
@@ -1723,6 +1722,10 @@ void Smt2Printer::toStreamCmdDefineFunctionRec(
   {
     out << ") (";
   }
+  else
+  {
+    out << " ";
+  }
   for (unsigned i = 0, size = formulas.size(); i < size; i++)
   {
     if (i > 0)