diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-06 22:48:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-06 22:48:13 -0500 |
| commit | 82f5610afdf5a45404e6acecfc117bb29f98963f (patch) | |
| tree | 32a5aa23a9a471f45017f11f451d559c68cf4bf4 /src/printer | |
| parent | 5ce47c94e28028493ab648eabac4b21302b41129 (diff) | |
Cleanup deprecated quantifiers attribute features (#4215)
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6e4fcb63a..b5e137b4d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -878,14 +878,7 @@ void Smt2Printer::toStream(std::ostream& out, { for (const Node& nc : n) { - if (nc.getKind() == kind::INST_ATTRIBUTE) - { - if (nc[0].getAttribute(theory::FunDefAttribute())) - { - out << ":fun-def"; - } - } - else if (nc.getKind() == kind::INST_PATTERN) + if (nc.getKind() == kind::INST_PATTERN) { out << ":pattern " << nc; } |