From 83af1ef582a7ff3749126a5d91d5ef0ac34c1516 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Nov 2020 17:03:30 -0600 Subject: [PATCH] Fix printing of define named function (#5425) Fixes the case where the type of the function is not a function type. --- src/smt/command.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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()); } -- 2.30.2