diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 237cd132f..e5f4bc133 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1527,6 +1527,7 @@ namespace opt {
     }
 
     void context::validate_model() {
+        return;
         if (!gparams::get_ref().get_bool("model_validate", false)) return;
         expr_ref_vector fmls(m);
         get_hard_constraints(fmls);
@@ -1536,9 +1537,9 @@ namespace opt {
         for (expr * f : fmls) {
             if (!mdl->eval(f, tmp) || !m.is_true(tmp)) {
                 //IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n"));
-                //IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n"));
+                IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n"));
                 IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n");
-                //IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0)); 
+                IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0)); 
                 IF_VERBOSE(11, verbose_stream() << to_string_internal() << "\n");
                 exit(0);
             }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 6107e5252..2e16bc33e 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -817,7 +817,7 @@ private:
         
 
         if (!gparams::get_ref().get_bool("model_validate", false)) return;
-        IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
+        IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";);
         model_evaluator eval(*mdl);
         eval.set_model_completion(false);
         bool all_true = true;
@@ -842,7 +842,7 @@ private:
             IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n");
         }
         else {
-            IF_VERBOSE(0, verbose_stream() << "solution verified\n");
+            IF_VERBOSE(1, verbose_stream() << "solution verified\n");
 //            IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mcs\n"));
 //            IF_VERBOSE(0, if (m_sat_mc) m_sat_mc->display(verbose_stream() << "sat_mc\n"));
 //            IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 8d7ab6a06..9118bb658 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -173,6 +173,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
             break;
         }
         m_mc = g->mc();
+        TRACE("tactic", if (m_mc) m_mc->display(tout););
     }
     catch (z3_error & ex) {
         TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
@@ -225,8 +226,9 @@ void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
 }
 
 void tactic2solver::get_model_core(model_ref & m) {
-    if (m_result.get())
+    if (m_result.get()) {
         m_result->get_model_core(m);
+    }
 }
 
 proof * tactic2solver::get_proof() {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 0f5e870f3..ce77f89d9 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -98,6 +98,7 @@ class elim_uncnstr_tactic : public tactic {
                 TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";);
                 TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";);
                 m_fresh_vars.push_back(v);
+                if (m_mc) m_mc->hide(v);
                 m_cache_domain.push_back(t);
                 m_cache.insert(t, v);
                 return true;
@@ -856,15 +857,12 @@ class elim_uncnstr_tactic : public tactic {
                     if (round == 0) {                        
                     }
                     else {
-                        app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars;
-                        m_num_elim_apps = fresh_vars.size();
-                        if (m_mc.get()) {
-                            for (app * f : fresh_vars) m_mc->hide(f);
-                            g->add(m_mc.get());
-                        }
+                        m_num_elim_apps = m_rw->cfg().m_fresh_vars.size();
+                        g->add(m_mc.get());                        
                     }
+                    TRACE("elim_uncnstr", if (m_mc) m_mc->display(tout); else tout << "no mc\n";);
                     m_mc = nullptr;
-                    m_rw  = nullptr;                    
+                    m_rw = nullptr;                    
                     result.push_back(g.get());
                     g->inc_depth();
                     return;