diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-09 11:40:59 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-09 11:40:59 -0800 |
commit | c6085d9b70beb9a2be5a26a3c085b4f1a1758410 (patch) | |
tree | 71f9fc4d9df2264994f34dabf77fd16de90ea851 /src/printer/smt2 | |
parent | 6330388f2606e82c4348de9ba6c62c4de7861cd9 (diff) |
Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)
Diffstat (limited to 'src/printer/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e025c64f1..8c9680a74 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1210,6 +1210,7 @@ void Smt2Printer::toStream(std::ostream& out, || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<GetProofCommand>(out, c) + || tryToStream<GetUnsatAssumptionsCommand>(out, c) || tryToStream<GetUnsatCoreCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant) || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) @@ -1803,6 +1804,11 @@ static void toStream(std::ostream& out, const GetProofCommand* c) out << "(get-proof)"; } +static void toStream(std::ostream& out, const GetUnsatAssumptionsCommand* c) +{ + out << "(get-unsat-assumptions)"; +} + static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) { out << "(get-unsat-core)"; |