diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 6b0eb1a7c..c9d046197 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -79,21 +79,27 @@ namespace sat {
         //SASSERT(!m_solver || m_solver->check_clauses(m));
         while (it != begin) {
             --it;
-            SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
-            // if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef,
+            bool_var v0 = it->var();
+            SASSERT(it->get_kind() != ELIM_VAR || m[v0] == l_undef);
+            // if it->get_kind() == BLOCK_LIT, then it might be the case that m[v] != l_undef,
             // and the following procedure flips its value.
             bool sat = false;
             bool var_sign = false;
             unsigned index = 0;
             literal_vector clause;
-            VERIFY(legal_to_flip(it->var()));
+            VERIFY(legal_to_flip(v0));
             for (literal l : it->m_clauses) {
                 if (l == null_literal) {
                     // end of clause
+                    if (v0 == 36858) 
+                        IF_VERBOSE(0, verbose_stream() << "clause: " << clause << "\n";
+                                   for (literal lit : clause) verbose_stream() << m[lit.var()] << " ";
+                                   verbose_stream() << "\n";);
+
                     elim_stack* st = it->m_elim_stack[index];
                     if (!sat) {     
-                        VERIFY(legal_to_flip(it->var()));                        
-                        m[it->var()] = var_sign ? l_false : l_true;
+                        VERIFY(legal_to_flip(v0));                        
+                        m[v0] = var_sign ? l_false : l_true;
                     }
                     if (st) {
                         process_stack(m, clause, st->stack());
@@ -115,11 +121,11 @@ namespace sat {
                 bool_var v = l.var();
                 if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n";
                 VERIFY(v < m.size());
-                if (v == it->var())
+                if (v == v0)
                     var_sign = sign;
                 if (value_at(l, m) == l_true)
                     sat = true;
-                else if (!sat && v != it->var() && m[v] == l_undef) {
+                else if (!sat && v != v0 && m[v] == l_undef) {
                     VERIFY(legal_to_flip(v));
                     // clause can be satisfied by assigning v.
                     m[v] = sign ? l_false : l_true;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 6ef0be83a..642fca348 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1007,7 +1007,7 @@ namespace sat {
         }
 
         bool process_var(bool_var v) {
-            return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
+            return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef;
         }
 
         enum elim_type {
@@ -1184,7 +1184,7 @@ namespace sat {
                 if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
                 if (s.is_marked(lit)) idx = i; 
             }
-            if (_blocked.var() == 16774 && false) {
+            if (false && _blocked.var() == 16774) {
                 IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n";
                            verbose_stream() << "tautology: " << m_tautology << "\n";
                            verbose_stream() << "index: " << idx << "\n";
@@ -1232,7 +1232,7 @@ namespace sat {
             // unsigned sz0 = m_covered_clause.size();
             m_covered_clause.resize(j);
             VERIFY(j >= m_clause.size());
-            if (_blocked.var() == 16774 && false) {
+            if (false && _blocked.var() == 16774) {
                 IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n");
             }
             // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 1617b487b..7def379e0 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -333,13 +333,6 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
-#if 0
-        if ((l1 == literal(5981, false) && l2 == literal(16764, false)) ||
-            (l2 == literal(5981, false) && l1 == literal(16764, false))) {
-            IF_VERBOSE(0, display(verbose_stream()));
-            //VERIFY(false);
-        }
-#endif
         if (find_binary_watch(get_wlist(~l1), ~l2)) {
             assign(l1, justification());
             return;
@@ -487,6 +480,8 @@ namespace sat {
         return reinit;
     }
 
+    static unsigned s_count = 0;
+
     void solver::attach_clause(clause & c, bool & reinit) {
         SASSERT(c.size() > 2);
         reinit = false;
@@ -1674,7 +1669,9 @@ namespace sat {
             if (!m_clone->check_model(m_model)) {
                 //IF_VERBOSE(0, display(verbose_stream()));
                 //IF_VERBOSE(0, display_watches(verbose_stream()));
-                //IF_VERBOSE(0, m_mc.display(verbose_stream()));
+                IF_VERBOSE(0, m_mc.display(verbose_stream()));
+                IF_VERBOSE(0, display_units(verbose_stream()));
+                //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n"));
                 throw solver_exception("check model failed (for cloned solver)");
             }
         }
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index 785ecb57e..5474700c3 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -52,7 +52,7 @@ struct bit_blaster_model_converter : public model_converter {
             m_newbits.push_back(f);
     }
     
-    virtual ~bit_blaster_model_converter() {
+    ~bit_blaster_model_converter() override {
     }
     
     void collect_bits(obj_hashtable<func_decl> & bits) {
@@ -123,10 +123,7 @@ struct bit_blaster_model_converter : public model_converter {
                     SASSERT(is_uninterp_const(bit));
                     func_decl * bit_decl = to_app(bit)->get_decl();
                     expr * bit_val = old_model->get_const_interp(bit_decl);
-                    if (bit_val == 0) {
-                        goto bail;
-                    }
-                    if (m().is_true(bit_val))
+                    if (bit_val != nullptr && m().is_true(bit_val))
                         val++;
                 }
             }
@@ -141,18 +138,12 @@ struct bit_blaster_model_converter : public model_converter {
                     func_decl * bit_decl = to_app(bit)->get_decl();
                     expr * bit_val = old_model->get_const_interp(bit_decl);
                     // remark: if old_model does not assign bit_val, then assume it is false.
-                    if (bit_val == 0) {
-                        goto bail;
-                    }
-                    if (!util.is_zero(bit_val))
+                    if (bit_val != nullptr && !util.is_zero(bit_val))
                         val++;
                 }
             }
             new_val = util.mk_numeral(val, bv_sz);
             new_model->register_decl(m_vars.get(i), new_val);
-            continue;
-        bail:
-            new_model->register_decl(m_vars.get(i), mk_bv(bs, *old_model));                                    
         }
     }
 
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 7e64b9c2c..b762f6b09 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -40,6 +40,7 @@ Notes:
 #include "tactic/smtlogics/qfbv_tactic.h"
 #include "solver/tactic2solver.h"
 #include "tactic/bv/bv_bound_chk_tactic.h"
+#include "ackermannization/ackermannize_bv_tactic.h"
 ///////////////
 
 class qfufbv_ackr_tactic : public tactic {
@@ -158,13 +159,14 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
 
 static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
     return and_then(mk_simplify_tactic(m),
-        mk_propagate_values_tactic(m),
-        mk_solve_eqs_tactic(m),
-        mk_elim_uncnstr_tactic(m),
-        if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
-        if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
-        mk_max_bv_sharing_tactic(m)
-        );
+                    mk_propagate_values_tactic(m),
+                    mk_solve_eqs_tactic(m),
+                    mk_elim_uncnstr_tactic(m),
+                    if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
+                    if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+                    mk_max_bv_sharing_tactic(m),
+                    if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p)))
+                    );
 }
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {