diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 7bbe4d29c..86b7e477d 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -436,9 +436,9 @@ public:
 
     virtual model_converter_ref get_model_converter() const {
         const_cast<inc_sat_solver*>(this)->convert_internalized();
+        if (m_cached_mc)
+            return m_cached_mc;
         if (m_internalized && m_internalized_converted) {            
-            if (m_cached_mc)
-                return m_cached_mc;
             m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
             m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
             m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
@@ -452,7 +452,6 @@ public:
     void convert_internalized() {
         if (!m_internalized || m_internalized_converted) return;
         sat2goal s2g;
-        m_sat_mc = nullptr;
         m_cached_mc = nullptr;
         goal g(m, false, true, false);
         s2g(m_solver, m_map, m_params, g, m_sat_mc);
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index a954f08c0..75892d12b 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -1183,8 +1183,8 @@ struct sat2goal::imp {
         ref<sat_model_converter> _mc;
         if (r.models_enabled()) {
             _mc = alloc(sat_model_converter, m, s);
+            mc = _mc.get();            
         }
-        mc = _mc.get();
         init_lit2expr(s, map, _mc);
         // collect units
         unsigned num_vars = s.num_vars();