2 files changed, 23 insertions, 1 deletions
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 5fc9b7ed8..102419ec4 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -23,6 +23,8 @@
 #include "expr/expr.h" // for ExprSetDepth etc..
 #include "expr/node_manager.h" // for VarNameAttr
 #include "options/language.h" // for LANG_AST
+#include "options/smt_options.h" // for unsat cores
+#include "smt/smt_engine.h"
 #include "smt/command.h"
 
 using namespace std;
@@ -58,7 +60,22 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c)
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
-
+void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const throw() {
+  out << "% SZS output start UnsatCore " << std::endl;
+  SmtEngine * smt = core.getSmtEngine();
+  Assert( smt!=NULL );
+  for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
+    std::string name;
+    if (smt->getExpressionName(*i, name)) {
+      // Named assertions always get printed
+      out << name << endl;
+    } else if (options::dumpUnsatCoresFull()) {
+      // Unnamed assertions only get printed if the option is set
+      out << *i << endl;
+    }
+  }
+  out << "% SZS output end UnsatCore " << std::endl;
+}
 
 }/* CVC4::printer::tptp namespace */
 }/* CVC4::printer namespace */
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index 7c8ddbd20..731885068 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -35,6 +35,11 @@ public:
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const Model& m) const throw();
+  /** print unsat core to stream
+  * We use the expression names stored in the SMT engine associated with the unsat core
+  * with UnsatCore::getSmtEngine.
+  */
+  void toStream(std::ostream& out, const UnsatCore& core) const throw();
 };/* class TptpPrinter */
 
 }/* CVC4::printer::tptp namespace */