diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index d030394a8..fe6d7e0f7 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -673,25 +673,33 @@ namespace bv {
         for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i)
             if (find(i) != i)
                 result->m_find.set_root(i, find(i));
-        result->m_prop_queue.append(m_prop_queue);
-        for (unsigned i = 0; i < m_bool_var2atom.size(); ++i) {
-            atom* a = m_bool_var2atom[i];
-            if (!a)
-                continue;
 
-            atom* new_a = new (result->get_region()) atom(i);
-            result->m_bool_var2atom.setx(i, new_a, nullptr);
-            for (auto vp : *a)
-                new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs);
-            for (eq_occurs const& occ : a->eqs()) {
+        auto clone_atom = [&](atom const& a) {
+            atom* new_a = new (result->get_region()) atom(a.m_bv);
+            result->m_bool_var2atom.setx(a.m_bv, new_a, nullptr);
+            for (auto [v, p] : a)
+                new_a->m_occs = new (result->get_region()) var_pos_occ(v, p, new_a->m_occs);
+            for (eq_occurs const& occ : a.eqs()) {
                 expr* e = occ.m_node->get_expr();
                 expr_ref e2(tr(e), tr.to());
                 euf::enode* n = ctx.get_enode(e2);
+                SASSERT(tr.to().contains(e2));
                 new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs);
             }
-            new_a->m_def = a->m_def;
-            new_a->m_var = a->m_var;
-            // validate_atoms();
+            new_a->m_def = a.m_def;
+            new_a->m_var = a.m_var;           
+        };
+
+        for (atom* a : m_bool_var2atom) 
+            if (a)
+                clone_atom(*a);
+        // validate_atoms();        
+
+        for (auto p : m_prop_queue) {
+            propagation_item q = p;
+            if (p.is_atom())
+                q = propagation_item(result->get_bv2a(p.m_atom->m_bv));
+            result->m_prop_queue.push_back(q);
         }
         return result;
     }
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 3d15c2cf1..f699a8030 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -161,11 +161,11 @@ namespace bv {
 
         struct atom {
             bool_var      m_bv;
-            eq_occurs*    m_eqs;
-            var_pos_occ * m_occs;
+            eq_occurs*    m_eqs = nullptr;
+            var_pos_occ * m_occs = nullptr;
             svector<std::pair<atom*, eq_occurs*>> m_bit2occ;
-            literal    m_var { sat::null_literal };
-            literal    m_def { sat::null_literal };
+            literal    m_var = sat::null_literal;
+            literal    m_def = sat::null_literal;
             atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {}
             ~atom() { m_bit2occ.clear(); }
             var_pos_it begin() const { return var_pos_it(m_occs); }
@@ -174,11 +174,12 @@ namespace bv {
         };
 
         struct propagation_item {
-            var_pos m_vp { var_pos(0, 0) };
-            atom* m_atom{ nullptr };
+            var_pos m_vp = var_pos(0, 0) ;
+            atom* m_atom = nullptr;
             explicit propagation_item(atom* a) : m_atom(a) {}
             explicit propagation_item(var_pos const& vp) : m_vp(vp) {}            
             bool operator==(propagation_item const& other) const { if (m_atom) return m_atom == other.m_atom; return false; }
+            bool is_atom() const { return m_atom != nullptr; }
         };