diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index 4fc9c09f3..1b32e9b3a 100644
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@@ -445,13 +445,14 @@ namespace euf {
                         delta += width(arg);
                     }
                 }
-            }
-            for (auto p : euf::enode_parents(n->get_root())) {
-                if (bv.is_extract(p->get_expr(), lo, hi, e)) {
-                    SASSERT(g.find(e)->get_root() == n->get_root());
-                    m_todo.push_back({ p, offset + lo });
+                for (auto p : euf::enode_parents(sib)) {
+                    if (bv.is_extract(p->get_expr(), lo, hi, e)) {
+                        SASSERT(g.find(e)->get_root() == n->get_root());
+                        m_todo.push_back({ p, offset + lo });
+                    }
                 }
             }
+
         }
         clear_offsets();
     }
@@ -475,17 +476,17 @@ namespace euf {
                     auto child = g.find(e);
                     m_todo.push_back({ child, offset + lo });
                 }
-            }
-            for (auto p : euf::enode_parents(n->get_root())) {
-                if (bv.is_concat(p->get_expr())) {
-                    unsigned delta = 0;
-                    for (unsigned j = p->num_args(); j-- > 0; ) {
-                        auto arg = p->get_arg(j);
-                        if (arg->get_root() == n->get_root()) 
-                            m_todo.push_back({ p, offset + delta });
-                        delta += width(arg);                   
+                for (auto p : euf::enode_parents(sib)) {
+                    if (bv.is_concat(p->get_expr())) {
+                        unsigned delta = 0;
+                        for (unsigned j = p->num_args(); j-- > 0; ) {
+                            auto arg = p->get_arg(j);
+                            if (arg->get_root() == n->get_root())
+                                m_todo.push_back({ p, offset + delta });
+                            delta += width(arg);
+                        }
                     }
-                }
+                }            
             }
         }
         clear_offsets();
@@ -524,6 +525,9 @@ namespace euf {
                     m_offsets.reserve(n->get_root_id() + 1);
                     m_offsets[n->get_root_id()].reset();
                 }
+                for (auto const& off : m_offsets) {
+                    SASSERT(off.empty());
+                }
                 m_jtodo.reset();
                 return;
             }
@@ -538,17 +542,23 @@ namespace euf {
                         delta += width(arg);
                     }
                 }
-            }
-            for (auto p : euf::enode_parents(n->get_root())) {
-                if (bv.is_extract(p->get_expr(), lo, hi, e)) {
-                    SASSERT(g.find(e)->get_root() == n->get_root());
-                    unsigned j2 = just.size();
-                    just.push_back({ g.find(e), n, j});
-                    m_jtodo.push_back({ p, offs + lo, j2});
+                for (auto p : euf::enode_parents(sib)) {
+                    if (bv.is_extract(p->get_expr(), lo, hi, e)) {
+                        SASSERT(g.find(e)->get_root() == n->get_root());
+                        unsigned j2 = just.size();
+                        just.push_back({ g.find(e), n, j });
+                        m_jtodo.push_back({ p, offs + lo, j2 });
+                    }
                 }
             }
-        }
 
+        }
+        IF_VERBOSE(0,
+            g.display(verbose_stream());
+            verbose_stream() << g.bpp(a) << " offset " << offset << " " << g.bpp(b) << "\n";
+            for (auto const& [n, offset, j] : m_jtodo) 
+                verbose_stream() << g.bpp(n) << " offset " << offset << " " << g.bpp(n->get_root()) << "\n";            
+        );
         UNREACHABLE();
     }
 
diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp
index fa0f27d1a..b0d97d56c 100644
--- a/src/sat/smt/polysat_egraph.cpp
+++ b/src/sat/smt/polysat_egraph.cpp
@@ -94,22 +94,24 @@ namespace polysat {
 
     // walk the e-graph to retrieve fixed overlaps
     void solver::get_fixed_bits(pvar pv, fixed_bits_vector& out) {
+        theory_var v = m_pddvar2var[pv];
+        euf::enode* b = var2enode(v);
         std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
-            n = n->get_root();
-            if (!n->interpreted())
+            auto r = n->get_root();
+            if (!r->interpreted())
                 return true;
-            auto w = n->get_th_var(get_id());
+            auto w = r->get_th_var(get_id());
             if (w == euf::null_theory_var)
                 return true;
-            unsigned length = bv.get_bv_size(n->get_expr());
+            unsigned length = bv.get_bv_size(r->get_expr());
             rational value;
-            VERIFY(bv.is_numeral(n->get_expr(), value));
+            VERIFY(bv.is_numeral(r->get_expr(), value));
             out.push_back({ fixed_slice(value, offset, length) });
             return false;
         };
-        theory_var v = m_pddvar2var[pv];        
-        m_bv_plugin->sub_slices(var2enode(v), consume_slice);
-        m_bv_plugin->super_slices(var2enode(v), consume_slice);
+   
+        m_bv_plugin->sub_slices(b, consume_slice);
+        m_bv_plugin->super_slices(b, consume_slice);
     }
     
     void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 5a167d166..244e90b41 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -135,6 +135,10 @@ namespace polysat {
     }
 
     void solver::explain_dep(dependency const& d, euf::enode_pair_vector& eqs, sat::literal_vector& core) {
+        std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
+            eqs.push_back({ a, b });
+            };
+
         if (d.is_axiom())
             ;
         else if (d.is_bool_var()) {
@@ -144,16 +148,10 @@ namespace polysat {
         }
         else if (d.is_fixed_claim()) {
             auto const& o = d.fixed();
-            std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
-                eqs.push_back({ a, b });
-                };
             explain_fixed(o.v, o, consume);
         }
         else if (d.is_offset_claim()) {
             auto const& offs = d.offset();
-            std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
-                eqs.push_back({ a, b });
-                };
             explain_slice(offs.v, offs.w, offs.offset, consume);
         }
         else {