5 files changed, 50 insertions, 1 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 3f93106a0..ed5116bc6 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -169,6 +169,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << "{} :: " << n.getConst<EmptySet>().getType();
       break;
 
+    case kind::STORE_ALL: {
+      const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
+      out << "ARRAY(" << asa.getType().getIndexType() << " OF "
+          << asa.getType().getConstituentType() << ") : " << asa.getExpr();
+      break;
+    }
+
     default:
       // Fall back to whatever operator<< does on underlying type; we
       // might luck out and print something reasonable.
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 8f0f50daa..dd2e180e1 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -153,4 +153,17 @@ void Printer::toStream(std::ostream& out, const Model& m) const throw() {
   }
 }/* Printer::toStream(Model) */
 
+void Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
+  std::map<Expr, std::string> names;
+  toStream(out, core, names);
+}/* Printer::toStream(UnsatCore) */
+
+void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() {
+  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
+    AssertCommand cmd(*i);
+    toStream(out, &cmd, -1, false, -1);
+    out << std::endl;
+  }
+}/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */
+
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index beb2438e2..e0b80ddfc 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -19,6 +19,9 @@
 #ifndef __CVC4__PRINTER__PRINTER_H
 #define __CVC4__PRINTER__PRINTER_H
 
+#include <map>
+#include <string>
+
 #include "util/language.h"
 #include "util/sexpr.h"
 #include "util/model.h"
@@ -103,6 +106,12 @@ public:
   /** Write a Model out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const Model& m) const throw();
 
+  /** Write an UnsatCore out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
+
+  /** Write an UnsatCore out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
+
 };/* class Printer */
 
 /**
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() << ")";
 }
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index e86b3cb2b..dbbc67fc2 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -37,7 +37,6 @@ class Smt2Printer : public CVC4::Printer {
 
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
   void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-  void toStream(std::ostream& out, const Model& m) const throw();
 public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
   using CVC4::Printer::toStream;
@@ -46,6 +45,8 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const Result& r) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
+  void toStream(std::ostream& out, const Model& m) const throw();
+  void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */