Fix printing of define named function (#5425)

Fixes the case where the type of the function is not a function type.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f1490e2f983d7f817a3cf85276859928e9e0f565..1e7401fa448e418bd61caf1aacc04c7228140cd7 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1313,11 +1313,18 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out,
                                           size_t dag,
                                           OutputLanguage language) const
 {
+  // get the range type of the function, or the type itself
+  // if its not a function
+  TypeNode range = d_func.getSort().getTypeNode();
+  if (range.isFunction())
+  {
+    range = range.getRangeType();
+  }
   Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
       out,
       d_func.toString(),
       api::termVectorToNodes(d_formals),
-      d_func.getSort().getFunctionCodomainSort().getTypeNode(),
+      range,
       d_formula.getNode());
 }