diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 60aadf8a1..dc63c2943 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -714,7 +714,6 @@ namespace sat {
         //
         // -----------------------
     public:
-        void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
         bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit;  }
         bool is_probing() const { return m_is_probing; }
         bool is_free(bool_var v) const { return m_free_vars.contains(v); }
diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp
index 18f0bd951..88cca5257 100644
--- a/src/sat/smt/bv_ackerman.cpp
+++ b/src/sat/smt/bv_ackerman.cpp
@@ -57,8 +57,8 @@ namespace bv {
             remove(other);
             add_cc(v1, v2);
         }
-        else if (other->m_count > m_propagate_high_watermark) 
-            s.s().set_should_simplify();
+        else if (other->m_count > 2*m_propagate_high_watermark) 
+            propagate();
     }
 
     void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
@@ -76,8 +76,8 @@ namespace bv {
             new_tmp();
             gc();
         }
-        if (other->m_count > m_propagate_high_watermark) 
-            s.s().set_should_simplify();
+        if (other->m_count > 2*m_propagate_high_watermark) 
+            propagate();
     }
 
     void ackerman::update_glue(vv& v) {
@@ -137,6 +137,9 @@ namespace bv {
         if (m_num_propagations_since_last_gc <= s.get_config().m_dack_gc) 
             return;
         m_num_propagations_since_last_gc = 0;
+
+        if (m_table.size() > m_gc_threshold) 
+            propagate();
         
         while (m_table.size() > m_gc_threshold) 
             remove(m_queue->prev());     
@@ -147,7 +150,6 @@ namespace bv {
     }
 
     void ackerman::propagate() {
-        SASSERT(s.s().at_base_lvl());
         auto* n = m_queue;
         vv* k = nullptr;
         unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflict * s.get_config().m_dack_factor);
diff --git a/src/sat/smt/bv_ackerman.h b/src/sat/smt/bv_ackerman.h
index f6465abc7..aab4053a2 100644
--- a/src/sat/smt/bv_ackerman.h
+++ b/src/sat/smt/bv_ackerman.h
@@ -51,13 +51,13 @@ namespace bv {
 
         solver&       s;
         table_t       m_table;
-        vv*           m_queue { nullptr };
-        vv*           m_tmp_vv { nullptr };
+        vv*           m_queue = nullptr;
+        vv*           m_tmp_vv = nullptr;
 
-        unsigned      m_gc_threshold { 100 };
-        unsigned      m_propagate_high_watermark { 10000 };
-        unsigned      m_propagate_low_watermark { 10 };
-        unsigned      m_num_propagations_since_last_gc { 0 };
+        unsigned      m_gc_threshold = 100;
+        unsigned      m_propagate_high_watermark = 10000;
+        unsigned      m_propagate_low_watermark = 10;
+        unsigned      m_num_propagations_since_last_gc = 0;
         bool_vector   m_diff_levels;
 
         void update_glue(vv& v);