From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Nov 2020 23:03:30 +0000 (-0600)
Subject: Fix printing of define named function (#5425)
X-Git-Tag: cvc5-1.0.0~2604
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=83af1ef582a7ff3749126a5d91d5ef0ac34c1516;p=cvc5.git

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 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());
 }