diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
index 87fa291db..37dce5937 100644
--- a/src/sat/sat_cut_simplifier.cpp
+++ b/src/sat/sat_cut_simplifier.cpp
@@ -168,7 +168,7 @@ namespace sat {
             aig2clauses();
             ++i;
         }
-        while ((force || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
+        while (((force && i < 5) || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
     }
 
     /**
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 492e27c9e..d9329a137 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -826,6 +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););
                 return;
             }
             modified = false;
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 9cf565c09..236f488c7 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -73,9 +73,9 @@ public:
         if (o == l_false) resg->assert_expr(m.mk_false());
         if (o != l_undef) result.push_back(resg.get());
         // report model
-        if (g->models_enabled() && (o == l_true)) {
+        if (g->models_enabled() && o == l_true) {
             model_ref abstr_model = imp.get_model();
-            g->add(mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model));
+            resg->add(mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model));
         }
     }