Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)

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)";