diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 3f5744556..5aab0b25f 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -61,6 +61,7 @@ class inc_sat_solver : public solver {
     model_converter_ref m_mc;
     model_converter_ref m_mc0;
     model_converter_ref m_sat_mc;
+    mutable model_converter_ref m_cached_mc;
     svector<double>     m_weights;
     std::string         m_unknown;
     // access formulas after they have been pre-processed and handled by the sat solver.
@@ -435,10 +436,12 @@ public:
     virtual model_converter_ref get_model_converter() const {
         const_cast<inc_sat_solver*>(this)->convert_internalized();
         if (m_internalized && m_internalized_converted) {            
-            model_converter_ref mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
-            mc = concat(solver::get_model_converter().get(), mc.get());
-            mc = concat(mc.get(), m_sat_mc.get());
-            return mc;
+            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());
+            return m_cached_mc;
         }
         else {
             return solver::get_model_converter();
@@ -449,6 +452,7 @@ public:
         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);
         m_internalized_fmls.reset();
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index a954f08c0..009d2818c 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -1030,6 +1030,7 @@ struct sat2goal::imp {
 
         void operator()(expr_ref& formula) override {
             if (!m_imc) {
+                std::cout << "create generic\n";
                 m_imc = alloc(generic_model_converter, m());
                 sat::literal_vector updates;
                 m_mc.expand(updates);
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 2556f40bd..2460557bc 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -40,7 +40,7 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum
     expr_ref_vector fmls(get_manager());
     stopwatch sw;
     sw.start();
-    get_assertions(fmls);
+    get_assertions(fmls);    
     ast_pp_util visitor(get_manager());
     model_converter_ref mc = get_model_converter();
     mc = concat(mc0(), mc.get());
@@ -194,7 +194,7 @@ void solver::assert_expr(expr* f, expr* t) {
     mc = concat(mc0(), mc.get());
     if (mc) {
         (*mc)(fml);        
-        // (*mc0())(a);        
+        // (*mc)(a);        
     }
     assert_expr_core(fml, a);    
 }
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index 9b8eed98d..ffc1ea09f 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -134,6 +134,7 @@ public:
 
 private:
     void flush_assertions() const {
+        if (m_assertions.empty()) return;
         m_rewriter.updt_params(get_params());
         proof_ref proof(m);
         expr_ref fml1(m), fml(m);