diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp
index 278dbb8f7..88fde3f83 100644
--- a/src/ackermannization/ackermannize_bv_tactic.cpp
+++ b/src/ackermannization/ackermannize_bv_tactic.cpp
@@ -35,7 +35,7 @@ public:
         tactic_report report("ackermannize_bv", *g);
         fail_if_unsat_core_generation("ackermannize", g);
         fail_if_proof_generation("ackermannize", g);
-        TRACE("ackermannize", g->display(tout << "in\n"););
+        TRACE("goal", g->display(tout << "in\n"););
 
         ptr_vector<expr> flas;
         const unsigned sz = g->size();
@@ -58,7 +58,7 @@ public:
         }
         
         resg->inc_depth();
-        TRACE("ackermannize", resg->display(tout << "out\n"););
+        TRACE("goal", resg->display(tout << "out\n"););
         SASSERT(resg->is_well_sorted());
     }
 
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index d239fe744..e845d620b 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -30,7 +30,8 @@ public:
           info(info),
           abstr_model(abstr_model),
           fixed_model(true)
-    { }
+    { 
+    }
 
     ackr_model_converter(ast_manager & m,
                          const ackr_info_ref& info)
@@ -44,6 +45,7 @@ public:
     void get_units(obj_map<expr, bool>& units) override { units.reset(); }
 
     void operator()(model_ref & md) override {
+        TRACE("ackermannize", tout << (fixed_model? "fixed" : "nonfixed") << "\n";);
         SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
         model_ref& old_model = fixed_model ? abstr_model : md;
         SASSERT(old_model.get());
@@ -100,6 +102,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination
         func_decl * const c = source->get_constant(i);
         app * const term = info->find_term(c);
         expr * value = source->get_const_interp(c);
+        TRACE("ackermannize", tout << mk_ismt2_pp(c, m) << " " << term << "\n";);
         if (!term) {
             destination->register_decl(c, value);
         }
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index bfeca6732..9ef324982 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -189,10 +189,17 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
             break;
         }
         if (m_mc && md) {
-            (*m_mc)(md);
+            // (*m_mc)(md);
+            
         }
+        TRACE("tactic", 
+              if (m_mc) m_mc->display(tout << "mc:");
+              if (g->mc()) g->mc()->display(tout << "g:");
+              if (md) tout << *md.get() << "\n";
+              );
+
         m_mc = concat(g->mc(), m_mc.get());
-        TRACE("tactic", if (m_mc) m_mc->display(tout););
+
     }
     catch (z3_error & ex) {
         TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index 6b332d7be..68633ba85 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -375,6 +375,7 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("bv-size-reduction", g);
     fail_if_unsat_core_generation("bv-size-reduction", g);
+    TRACE("goal", g->display(tout););
     result.reset();
     model_converter_ref mc;
     run(*(g.get()), mc);
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index d9329a137..4ecfb2f57 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -779,7 +779,7 @@ class elim_uncnstr_tactic : public tactic {
     void run(goal_ref const & g, goal_ref_buffer & result) {
         bool produce_proofs = g->proofs_enabled();
         
-        TRACE("elim_uncnstr_bug", g->display(tout););
+        TRACE("goal", g->display(tout););
         tactic_report report("elim-uncnstr", *g);
         m_vars.reset();
         collect_occs p;
@@ -826,7 +826,7 @@ class elim_uncnstr_tactic : public tactic {
                 m_rw = nullptr;                    
                 result.push_back(g.get());
                 g->inc_depth();
-                TRACE("elim_uncnstr_bug", g->display(tout););
+                TRACE("goal", g->display(tout););
                 return;
             }
             modified = false;
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index f639ca607..316d803a6 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -1007,7 +1007,7 @@ class solve_eqs_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             model_converter_ref mc;
             tactic_report report("solve_eqs", *g);
-            TRACE("solve_eqs", g->display(tout););
+            TRACE("goal", g->display(tout););
             m_produce_models = g->models_enabled();
             m_produce_proofs = g->proofs_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
@@ -1043,7 +1043,7 @@ class solve_eqs_tactic : public tactic {
             g->inc_depth();
             g->add(mc.get());
             result.push_back(g.get());
-            TRACE("solve_eqs", g->display(tout););
+            TRACE("goal", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
     };
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index a363313bc..0b972bb3e 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -337,6 +337,9 @@ void goal::display(ast_printer & prn, std::ostream & out) const {
         prn.display(out, form(i), 2);
     }
     out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+    if (m_mc) {
+        m_mc->display(out);
+    }
 }
 
 void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) const {
@@ -370,6 +373,9 @@ void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) cons
         out << ")";
     }
     out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+    if (m_mc) {
+        m_mc->display(out);
+    }
 }
 
 void goal::display_with_dependencies(std::ostream & out) const {
@@ -391,6 +397,9 @@ void goal::display_with_dependencies(std::ostream & out) const {
         out << "\n  " << mk_ismt2_pp(form(i), m(), 2);
     }
     out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+    if (m_mc) {
+        m_mc->display(out);
+    }
 }
 
 void goal::display(ast_printer_context & ctx) const {
@@ -409,6 +418,9 @@ void goal::display(std::ostream & out) const {
         out << mk_ismt2_pp(form(i), m(), 2);
     }
     out << ")" << std::endl;
+    if (m_mc) {
+        m_mc->display(out);
+    }
 }
 
 void goal::display_as_and(std::ostream & out) const {
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 236f488c7..7d22ef682 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -59,7 +59,7 @@ public:
         fail_if_unsat_core_generation("qfufbv_ackr", g);
         fail_if_proof_generation("qfufbv_ackr", g);
 
-        TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
+        TRACE("goal", g->display(tout););
         // running implementation
         ptr_vector<expr> flas;
         const unsigned sz = g->size();
@@ -106,7 +106,7 @@ private:
     bool                                 m_inc_use_sat;
 
     solver* setup_sat() {
-        solver * sat(nullptr);
+        solver * sat = nullptr;
         if (m_use_sat) {
             if (m_inc_use_sat) {
                 sat = mk_inc_sat_solver(m_m, m_p);