diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index d8041eb07..9b763ea98 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -249,7 +249,6 @@ namespace polysat {
     }
 #endif
 
-#if 1
     bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
         SASSERT_EQ(width(s1), width(s2));
         SASSERT(!has_sub(s1));
@@ -262,7 +261,7 @@ namespace polysat {
 #if 0
     bool slicing::merge_value(slice s0, rational val0, dep_t dep) {
         vector<std::pair<slice, rational>> todo;
-        todo.push_back({find(s0), std::move(val0)});
+        todo.push_back({s0->get_root(), std::move(val0)});
         // check compatibility for sub-slices
         for (unsigned i = 0; i < todo.size(); ++i) {
             auto const& [s, val] = todo[i];
@@ -278,8 +277,8 @@ namespace polysat {
             if (has_sub(s)) {
                 // s is split into [s.width-1, cut+1] and [cut, 0]
                 unsigned const cut = m_slice_cut[s];
-                todo.push_back({find_sub_lo(s), mod2k(val, cut + 1)});
-                todo.push_back({find_sub_hi(s), machine_div2k(val, cut + 1)});
+                todo.push_back({sub_lo(s)->get_root(), mod2k(val, cut + 1)});
+                todo.push_back({sub_hi(s)->get_root(), machine_div2k(val, cut + 1)});
             }
         }
         // all succeeded, so apply the values
@@ -339,8 +338,8 @@ namespace polysat {
             if (x == y)
                 continue;
             if (width(x) == width(y)) {
-                enode* const rx = find(x);
-                enode* const ry = find(y);
+                enode* const rx = x->get_root();
+                enode* const ry = y->get_root();
                 if (rx == ry)
                     explain_class(x, y, out_deps);
                 else {
@@ -351,7 +350,7 @@ namespace polysat {
                 }
             }
             else if (width(x) > width(y)) {
-                enode* const rx = find(x);
+                enode* const rx = x->get_root();
                 xs.push_back(sub_hi(rx));
                 xs.push_back(sub_lo(rx));
                 ys.push_back(y);
@@ -359,7 +358,7 @@ namespace polysat {
             else {
                 SASSERT(width(x) < width(y));
                 xs.push_back(x);
-                enode* const ry = find(y);
+                enode* const ry = y->get_root();
                 ys.push_back(sub_hi(ry));
                 ys.push_back(sub_lo(ry));
             }
@@ -441,8 +440,8 @@ namespace polysat {
         enode_vector& ys = m_tmp3;
         SASSERT(xs.empty());
         SASSERT(ys.empty());
-        find_base(x, xs);
-        find_base(y, ys);
+        get_root_base(x, xs);
+        get_root_base(y, ys);
         SASSERT(all_of(xs, [](enode* s) { return s->is_root(); }));
         SASSERT(all_of(ys, [](enode* s) { return s->is_root(); }));
         bool result = (xs == ys);
@@ -454,7 +453,7 @@ namespace polysat {
         return result;
     }
 
-    template <bool should_find>
+    template <bool should_get_root>
     void slicing::get_base_core(enode* src, enode_vector& out_base) const {
         enode_vector& todo = m_tmp1;
         SASSERT(todo.empty());
@@ -462,7 +461,7 @@ namespace polysat {
         while (!todo.empty()) {
             enode* s = todo.back();
             todo.pop_back();
-            if constexpr (should_find) {
+            if constexpr (should_get_root) {
                 s = s->get_root();
             }
             if (!has_sub(s))
@@ -479,7 +478,7 @@ namespace polysat {
         get_base_core<false>(src, out_base);
     }
 
-    void slicing::find_base(enode* src, enode_vector& out_base) const {
+    void slicing::get_root_base(enode* src, enode_vector& out_base) const {
         get_base_core<true>(src, out_base);
     }
 
@@ -659,7 +658,7 @@ namespace polysat {
             out << "v" << v << ":";
             base.reset();
             enode* const vs = var2slice(v);
-            find_base(vs, base);
+            get_root_base(vs, base);
             for (enode* s : base)
                 display(out << " ", s);
             // if (has_value(vs)) {
@@ -722,12 +721,11 @@ namespace polysat {
             }
             // if slice has a value, it should be propagated to its sub-slices
             // if (has_value(s)) {
-            //     VERIFY(has_value(find_sub_hi(s)));
-            //     VERIFY(has_value(find_sub_lo(s)));
+            //     VERIFY(has_value(sub_hi(s)->get_root()));
+            //     VERIFY(has_value(sub_lo(s)->get_root()));
             // }
         }
         return true;
     }
-#endif
 
 }
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 65279f32c..1dca27859 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -49,7 +49,7 @@ namespace polysat {
         struct slice_info {
             unsigned    width   = 0;            // number of bits in the slice
             unsigned    cut     = null_cut;     // cut point, or null_cut if no subslices
-            pvar        var     = null_var;     // slice is equivalent to this variable, if any
+            pvar        var     = null_var;     // slice is equivalent to this variable, if any (without dependencies)
             enode*      slice   = nullptr;      // if enode corresponds to a concat(...) expression, this field links to the represented slice.
             enode*      sub_hi  = nullptr;      // upper subslice s[|s|-1:cut+1]
             enode*      sub_lo  = nullptr;      // lower subslice s[cut:0]
@@ -67,8 +67,6 @@ namespace polysat {
         ast_manager             m_ast;
         sort_ref                m_slice_sort;
         func_decl_ref_vector    m_concat_decls;
-        // expr_ref_vector         m_expr_storage;
-        // unsigned_vector         m_expr_scopes;
 
         euf::egraph             m_egraph;
         slice_info_vector       m_info;         // indexed by enode::get_id()
@@ -113,32 +111,8 @@ namespace polysat {
         unsigned_vector m_slice_cut;
         // The sub-slices are at indices sub and sub+1 (or null_slice if there is no subdivision)
         slice_vector    m_slice_sub;
-
-        pvar_vector     m_slice2var;    // slice -> pvar, or null_var if slice is not equivalent to a variable
-        slice_vector    m_var2slice;    // pvar -> slice
-
-        ptr_vector<euf::enode>  m_slice2enode;
-        ptr_addr_map<euf::enode, slice> m_enode2slice;
 */
 
-#if 0
-        unsigned_vector m_mark;
-        unsigned        m_mark_timestamp = 0;
-#if Z3DEBUG
-        bool            m_mark_active = false;
-#endif
-
-        void begin_mark() {
-            DEBUG_CODE({ SASSERT(!m_mark_active); m_mark_active = true; });
-            m_mark_timestamp++;
-            if (!m_mark_timestamp)
-                m_mark_timestamp++;
-        }
-        void end_mark() { DEBUG_CODE({ SASSERT(m_mark_active); m_mark_active = false; }); }
-        bool is_marked(slice s) const { SASSERT(m_mark_active); return m_mark[s] == m_mark_timestamp; }
-        void mark(slice s) { SASSERT(m_mark_active); m_mark[s] = m_mark_timestamp; }
-#endif
-
         slice_info& info(euf::enode* n);
         slice_info const& info(euf::enode* n) const;
 
@@ -172,22 +146,19 @@ namespace polysat {
         void split(enode* s, unsigned cut);
         void split_core(enode* s, unsigned cut);
 
-        template <bool should_find>
+        template <bool should_get_root>
         void get_base_core(enode* src, enode_vector& out_base) const;
 
         /// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... ++ s_n (actual descendant subslices)
         void get_base(enode* src, enode_vector& out_base) const;
         /// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... ++ s_n (representatives of subslices)
-        void find_base(enode* src, enode_vector& out_base) const;
+        void get_root_base(enode* src, enode_vector& out_base) const;
 
         /// Retrieve (or create) base slices s_1,...,s_n such that src[hi:lo] == s_1 ++ ... ++ s_n.
         /// If output_full_src is true, return the new base for src, i.e., src == s_1 ++ ... ++ s_n.
         /// If output_base is false, return coarsest intermediate slices instead of only base slices.
         void mk_slice(enode* src, unsigned hi, unsigned lo, enode_vector& out, bool output_full_src = false, bool output_base = true);
 
-        /// Find representative
-        enode* find(enode* s) const { return s->get_root(); }
-
         // Merge equivalence classes of two base slices.
         // Returns true if merge succeeded without conflict.
         [[nodiscard]] bool merge_base(enode* s1, enode* s2, dep_t dep);