Fix printing of define named function (#5425)

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

1 files changed, 8 insertions, 1 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f1490e2f9..1e7401fa4 100644
--- 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());
 }