diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-03 09:42:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-03 09:42:15 -0500 |
commit | a41a4e978013665784649e968dae968751309e27 (patch) | |
tree | 98066f553cd835a8a40e58d35bd13f02cf2416c4 /src/printer | |
parent | 4051c9f2df3f83d7e09636f97ed56ed9579e557d (diff) | |
parent | b61070cf03c30abe3ba5956596b88464053ff358 (diff) |
Merge branch 'master' into issue6636
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4607d2747..04a57e0e9 100644 --- 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) |