diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-25 10:05:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-25 10:05:45 -0500 |
| commit | b2261930d0fa97f0b40e4f96313db957e8ab9418 (patch) | |
| tree | bf079d5260223e8f8304f7d898e3e115dd2dcbae | |
| parent | 78b3f62746e95b915436c6a9bb57dab7be4d4fa4 (diff) | |
Fix printing of instantiation patterns (#3305)
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 37a73db2d..df9bee981 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -861,7 +861,8 @@ void Smt2Printer::toStream(std::ostream& out, out << ')'; return; } - case kind::INST_PATTERN: break; + case kind::INST_PATTERN: + case kind::INST_NO_PATTERN: break; case kind::INST_PATTERN_LIST: { for (const Node& nc : n) @@ -873,10 +874,14 @@ void Smt2Printer::toStream(std::ostream& out, out << ":fun-def"; } } - else + else if (nc.getKind() == kind::INST_PATTERN) { out << ":pattern " << nc; } + else if (nc.getKind() == kind::INST_NO_PATTERN) + { + out << ":no-pattern " << nc[0]; + } } return; break; |