From 2313b14210bed44699212b1ba9358807b8525146 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Nov 2017 20:40:43 -0800
Subject: [PATCH] include mc0 for display method

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 6 ++++--
 src/solver/check_sat_result.h   | 2 +-
 src/solver/solver.cpp           | 9 +--------
 3 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 06a7cba19..8d23c5ef4 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -864,7 +864,8 @@ void cmd_context::insert(symbol const & s, object_ref * r) {
 }
 
 void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t) {
-    if (!m_mc0) m_mc0 = alloc(generic_model_converter, m());
+    if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m());
+    if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get()); 
     func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m());
     dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
     func_decls & fs = e->get_data().m_value;
@@ -873,7 +874,8 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai
 }
 
 void cmd_context::model_del(func_decl* f) {
-    if (!m_mc0) m_mc0 = alloc(generic_model_converter, m());
+    if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m());
+    if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get()); 
     m_mc0->hide(f);
 }
 
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index 572c4d88d..4ea28ee61 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -57,7 +57,7 @@ public:
         r.append(core.size(), core.c_ptr());
     }
     void set_model_converter(model_converter* mc) { m_mc0 = mc; }
-    model_converter* mc0() { return m_mc0.get(); }
+    model_converter* mc0() const { return m_mc0.get(); }
     virtual void get_model_core(model_ref & m) = 0;
     void get_model(model_ref & m) {
         get_model_core(m);
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index f14467337..3d36fb01e 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -40,27 +40,20 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum
     expr_ref_vector fmls(get_manager());
     stopwatch sw;
     sw.start();
-    // std::cout << "display 1\n";
     get_assertions(fmls);
-    // std::cout << "display 2 " << sw.get_current_seconds() << "\n";
     ast_pp_util visitor(get_manager());
     model_converter_ref mc = get_model_converter();
-    // std::cout << "display 3 " << sw.get_current_seconds() << "\n";
+    mc = concat(mc0(), mc.get());
     if (mc.get()) { 
         mc->collect(visitor); 
     }
-    // std::cout << "display 4 " << sw.get_current_seconds() << "\n";
     visitor.collect(fmls);
-    // std::cout << "display 5 " << sw.get_current_seconds() << "\n";
     visitor.collect(n, assumptions);
     visitor.display_decls(out);
-    // std::cout << "display 6 " << sw.get_current_seconds() << "\n";
     visitor.display_asserts(out, fmls, true);
-    // std::cout << "display 7 " << sw.get_current_seconds() << "\n";
     if (mc.get()) {
         mc->display(out);
     }
-    // std::cout << "display 8 " << sw.get_current_seconds() << "\n";
     return out;
 }