diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 637db3871..006d21e41 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -171,6 +171,7 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
     expr_dependency_ref core(m);
     std::string         reason_unknown = "unknown";
     labels_vec labels;
+    TRACE("tactic", g->display(tout););
     try {
         switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
         case l_true: 
@@ -189,14 +190,15 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
             }
             break;
         }
-        TRACE("tactic", 
-              if (m_mc) m_mc->display(tout << "mc:");
-              if (g->mc()) g->mc()->display(tout << "g:");
-              if (md) tout << *md.get() << "\n";
-              );
+        CTRACE("tactic", md.get(), tout << *md.get() << "\n";);
         if (m_mc && md) {
             (*m_mc)(md);
         }
+        TRACE("tactic", 
+              if (m_mc) m_mc->display(tout << "mc:\n");
+              if (g->mc()) g->mc()->display(tout << "\ng\n:");
+              if (md) tout << "\nmodel:\n" << *md.get() << "\n";
+              );
         m_mc = concat(g->mc(), m_mc.get());
 
     }
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index 89e2b6602..021bbc886 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -127,7 +127,18 @@ public:
     ~model2mc() override {}
 
     void operator()(model_ref & m) override {
-        m = m_model;
+        if (!m || !m_model) {
+            m = m_model;
+            return;
+        }
+        for (unsigned i = m_model->get_num_constants(); i-- > 0; ) {
+            func_decl* f = m_model->get_constant(i);
+            m->register_decl(f, m_model->get_const_interp(f));
+        }
+        for (unsigned i = m_model->get_num_functions(); i-- > 0; ) {
+            func_decl* f = m_model->get_function(i);
+            m->register_decl(f, m_model->get_func_interp(f));
+        }
     }
 
     void operator()(labels_vec & r) override {