diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-02 16:16:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-02 14:16:40 -0700 |
commit | 87b204084e86b534571f16250ca4871150b2a783 (patch) | |
tree | 6074f30a6aa13d0d46c9e40fac55a91238030eca /src/printer | |
parent | 9258aa062ebefb8af7727567470f9a387181d466 (diff) |
Fixes for printing define-fun-rec (#6673)
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) |