diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 264e28f55..7157e2d13 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -49,7 +49,6 @@ namespace smt {
         unsigned bv_size      = get_bv_size(n);
         bool is_relevant      = ctx.is_relevant(n);
         literal_vector & bits = m_bits[v];
-        TRACE("bv", tout << "v" << v << "\n";);
         bits.reset();
         m_bits_expr.reset();
 
@@ -65,6 +64,12 @@ namespace smt {
                 ctx.mark_as_relevant(b);
             }
         }
+
+        TRACE("bv", tout << "v" << v << " #" << owner->get_id() << "\n";
+              for (unsigned i = 0; i < bv_size; i++) 
+                  tout << mk_bounded_pp(m_bits_expr[i], m) << "\n";
+              );
+
     }
 
     class mk_atom_trail : public trail<theory_bv> {
@@ -217,12 +222,17 @@ namespace smt {
         }
     };
 
+    void theory_bv::add_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
+        if (!params().m_bv_eq_axioms)
+            return;
+        m_prop_diseqs.push_back(bv_diseq(v1, v2, idx));
+        ctx.push_trail(push_back_vector<context, svector<bv_diseq>>(m_prop_diseqs));
+    }
+
     /**
        \brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
     */
-    void theory_bv::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
-        if (!params().m_bv_eq_axioms)
-            return;
+    void theory_bv::assert_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
         SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
         TRACE("bv_diseq_axiom", tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2););
         // found new disequality
@@ -260,7 +270,7 @@ namespace smt {
             theory_var v2   = occs->m_var;
             unsigned   idx2 = occs->m_idx;
             if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v)) 
-                mk_new_diseq_axiom(v, v2, idx);
+                add_new_diseq_axiom(v, v2, idx);
             occs = occs->m_next;
         }
     }
@@ -1160,7 +1170,6 @@ namespace smt {
                 m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
                 m_diseq_watch_trail.push_back(watch_var);
                 return;
-                //m_replay_diseq.push_back(std::make_pair(v1, v2));            
             }
         }
 
@@ -1329,7 +1338,7 @@ namespace smt {
     }
 
     void theory_bv::relevant_eh(app * n) {
-        TRACE("bv", tout << "relevant: " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
+        TRACE("bv", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
         if (m.is_bool(n)) {
             bool_var v = ctx.get_bool_var(n);
             atom * a   = get_bv2a(v);
@@ -1355,6 +1364,8 @@ namespace smt {
             theory_var v = e->get_th_var(get_id());
             if (v != null_theory_var) {
                 literal_vector & bits        = m_bits[v];
+                TRACE("bv", tout << "mark bits relevant: " << bits.size() << ": " << bits << "\n";);
+                SASSERT(!is_bv(v) || bits.size() == get_bv_size(v));
                 for (literal lit : bits) {
                     ctx.mark_as_relevant(lit);
                 }
@@ -1543,7 +1554,7 @@ namespace smt {
                 // conflict was detected ... v1 and v2 have complementary bits
                 SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
                 SASSERT(m_bits[v1].size() == m_bits[v2].size());
-                mk_new_diseq_axiom(v1, v2, zo.m_idx);
+                add_new_diseq_axiom(v1, v2, zo.m_idx);
                 reset_merge_aux();
                 return false;
             }
@@ -1559,13 +1570,12 @@ namespace smt {
     }
 
     void theory_bv::propagate() {
-        unsigned sz = m_replay_diseq.size();
-        if (sz > 0) {
-            for (unsigned i = 0; i < sz; ++i) {
-                auto const& p = m_replay_diseq[i];
-                expand_diseq(p.first, p.second);
-            }
-            m_replay_diseq.reset();
+        if (!can_propagate())
+            return;
+        ctx.push_trail(value_trail<context, unsigned>(m_prop_diseqs_qhead));
+        for (; m_prop_diseqs_qhead < m_prop_diseqs.size() && !ctx.inconsistent(); ++m_prop_diseqs_qhead) {
+            auto p = m_prop_diseqs[m_prop_diseqs_qhead];
+            assert_new_diseq_axiom(p.v1, p.v2, p.idx);
         }
     }
 
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index bb4385114..76c78c930 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -125,7 +125,13 @@ namespace smt {
         mutable vector<rational>         m_power2;
         
         unsigned char            m_eq_activity[256];
-        svector<std::pair<theory_var, theory_var>> m_replay_diseq;
+        struct bv_diseq {
+            theory_var v1, v2;
+            unsigned idx;
+            bv_diseq(theory_var v1, theory_var v2, unsigned idx):v1(v1), v2(v2), idx(idx) {}
+        };
+        svector<bv_diseq> m_prop_diseqs;
+        unsigned          m_prop_diseqs_qhead { 0 };
         vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
         unsigned char            m_diseq_activity[256];
         svector<bool_var> m_diseq_watch_trail;
@@ -162,7 +168,8 @@ namespace smt {
         void get_arg_bits(app * n, unsigned idx, expr_ref_vector & r);
         friend class add_var_pos_trail;
         void simplify_bit(expr * s, expr_ref & r);
-        void mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
+        void add_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
+        void assert_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
         friend class register_true_false_bit_trail;
         void register_true_false_bit(theory_var v, unsigned idx);
         void find_new_diseq_axioms(var_pos_occ * occs, theory_var v, unsigned idx);
@@ -240,7 +247,7 @@ namespace smt {
         bool include_func_interp(func_decl* f) override;
         svector<theory_var>   m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
         bool merge_zero_one_bits(theory_var r1, theory_var r2);
-        bool can_propagate() override { return !m_replay_diseq.empty(); }
+        bool can_propagate() override { return m_prop_diseqs_qhead < m_prop_diseqs.size(); }
         void propagate() override;
 
         // -----------------------------------