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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4607d2747495a7bea06571052654b64d186a7378..04a57e0e9330be88bb56acc5ee7ab2d3b9dd239d 100644 (file)
--- 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)