Improved SMT-LIBv2 language support for unsat cores.

1 files changed, 10 insertions, 6 deletions

diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp
index 6344b3eda..929d5e909 100644
--- a/src/util/unsat_core.cpp
+++ b/src/util/unsat_core.cpp
@@ -30,15 +30,19 @@ UnsatCore::const_iterator UnsatCore::end() const {
 }
 
 void UnsatCore::toStream(std::ostream& out) const {
-  for(UnsatCore::const_iterator i = begin(); i != end(); ++i) {
-    out << AssertCommand(*i) << std::endl;
-  }
+  smt::SmtScope smts(d_smt);
+  Expr::dag::Scope scope(out, false);
+  Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
 }
 
-std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
-  smt::SmtScope smts(core.d_smt);
+void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const {
+  smt::SmtScope smts(d_smt);
   Expr::dag::Scope scope(out, false);
-  Printer::getPrinter(options::outputLanguage())->toStream(out, core);
+  Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names);
+}
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
+  core.toStream(out);
   return out;
 }