diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-09-29 16:32:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-29 21:32:31 +0000 |
| commit | bed236463f34019a802c8f0ee66f386b77ac4446 (patch) | |
| tree | b243c34aa9382f34f87c187ae136c000ac2d906e /src/printer/smt2/smt2_printer.cpp | |
| parent | 7d859b19c2755dc5071f4bedbbeab8a37870e69a (diff) | |
Remove support for extended `(check-sat <term>)` command. (#7270)
This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cf3f68308..e6aff1ace 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1363,23 +1363,9 @@ void Smt2Printer::toStreamCmdPop(std::ostream& out) const out << "(pop 1)" << std::endl; } -void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const +void Smt2Printer::toStreamCmdCheckSat(std::ostream& out) const { - if (!n.isNull()) - { - toStreamCmdPush(out); - out << std::endl; - toStreamCmdAssert(out, n); - out << std::endl; - toStreamCmdCheckSat(out); - out << std::endl; - toStreamCmdPop(out); - } - else - { - out << "(check-sat)"; - } - out << std::endl; + out << "(check-sat)" << std::endl; } void Smt2Printer::toStreamCmdCheckSatAssuming( |