diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index dc927e9f3..97b6d89d7 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -217,8 +217,10 @@ public:
                     m_ctx->get_model(md);
                     buffer<symbol> r;
                     m_ctx->get_relevant_labels(0, r);
+                    labels_vec rv;
+                    rv.append(r.size(), r.c_ptr());
                     model_converter_ref mc;
-                    mc = model_and_labels2model_converter(md.get(), r);
+                    mc = model_and_labels2model_converter(md.get(), rv);
                     mc = concat(fmc.get(), mc.get());
                     in->add(mc.get());
                 }
@@ -268,7 +270,9 @@ public:
                             m_ctx->get_model(md);
                             buffer<symbol> r;
                             m_ctx->get_relevant_labels(0, r);
-                            in->add(model_and_labels2model_converter(md.get(), r));
+                            labels_vec rv;
+                            rv.append(r.size(), r.c_ptr());
+                            in->add(model_and_labels2model_converter(md.get(), rv));
                         }
                         return;
                     default:
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 3d36fb01e..2556f40bd 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -179,6 +179,7 @@ bool solver::is_literal(ast_manager& m, expr* e) {
 void solver::assert_expr(expr* f) {
     expr_ref fml(f, get_manager());
     model_converter_ref mc = get_model_converter();
+    mc = concat(mc0(), mc.get());
     if (mc) {
         (*mc)(fml);        
     }
@@ -190,6 +191,7 @@ void solver::assert_expr(expr* f, expr* t) {
     expr_ref fml(f, m);
     expr_ref a(t, m);
     model_converter_ref mc = get_model_converter();
+    mc = concat(mc0(), mc.get());
     if (mc) {
         (*mc)(fml);        
         // (*mc0())(a);        
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 3a4573517..8befffff5 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -58,7 +58,7 @@ void generic_model_converter::display(std::ostream & out) {
         display_del(out, e.m_f);
     }
     for (entry const& e : m_add_entries) {
-        display_del(out, e.m_f);
+        display_add(out, m, e.m_f, e.m_def);
     }
 }
 
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index da6a0dcf8..2598aa4f1 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -96,11 +96,11 @@ model_converter * concat(model_converter * mc1, model_converter * mc2) {
 
 class model2mc : public model_converter {
     model_ref m_model;
-    buffer<symbol> m_labels;
+    labels_vec m_labels;
 public:
     model2mc(model * m):m_model(m) {}
 
-    model2mc(model * m, buffer<symbol> const & r):m_model(m), m_labels(r) {}
+    model2mc(model * m, labels_vec const & r):m_model(m), m_labels(r) {}
 
     virtual ~model2mc() {}
 
@@ -122,27 +122,25 @@ public:
     }
     
     void display(std::ostream & out) override {
-        out << "(model->model-converter-wrapper\n";
+        out << "(rmodel->model-converter-wrapper\n";
         model_v2_pp(out, *m_model);
         out << ")\n";
     }    
     
     virtual model_converter * translate(ast_translation & translator) {
         model * m = m_model->translate(translator);
-        return alloc(model2mc, m);
+        return alloc(model2mc, m, m_labels);
     }
 
 };
 
 model_converter * model2model_converter(model * m) {
-    if (m == 0)
-        return 0;
+    if (!m) return nullptr;
     return alloc(model2mc, m);
 }
 
-model_converter * model_and_labels2model_converter(model * m, buffer<symbol> & r) {
-    if (m == 0)
-        return 0;
+model_converter * model_and_labels2model_converter(model * m, labels_vec const & r) {
+    if (!m) return nullptr;
     return alloc(model2mc, m, r);
 }
 
diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h
index c768a0cae..d4991e672 100644
--- a/src/tactic/model_converter.h
+++ b/src/tactic/model_converter.h
@@ -98,7 +98,7 @@ model_converter * concat(model_converter * mc1, model_converter * mc2);
 
 model_converter * model2model_converter(model * m);
 
-model_converter * model_and_labels2model_converter(model * m, buffer<symbol> &r);
+model_converter * model_and_labels2model_converter(model * m, labels_vec const &r);
 
 void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m);