1 files changed, 19 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 903a1e6e3..3ca5674e9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -713,6 +713,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<GetProofCommand>(out, c) ||
+     tryToStream<GetUnsatCoreCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
      tryToStream<SetInfoCommand>(out, c) ||
@@ -781,6 +782,20 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 }/* Smt2Printer::toStream(CommandStatus*) */
 
 
+void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() {
+  out << "(" << std::endl;
+  for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
+    map<Expr, string>::const_iterator j = names.find(*i);
+    if(j == names.end()) {
+      out << *i << endl;
+    } else {
+      out << (*j).second << endl;
+    }
+  }
+  out << ")" << endl;
+}/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
+
+
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
   out << "(model" << endl;
   this->Printer::toStream(out, m);
@@ -1042,6 +1057,10 @@ static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
   out << "(get-proof)";
 }
 
+static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() {
+  out << "(get-unsat-core)";
+}
+
 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "(set-info :status " << c->getStatus() << ")";
 }