diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 2f7305174..14e4215bb 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -1363,7 +1363,7 @@ namespace polysat {
         SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); }));
     }
 
-    void slicing::collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_pair_vector& out_just) {
+    void slicing::collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_vector& out_just) {
         enode_vector& base = m_tmp2;
         SASSERT(base.empty());
         get_base(var2slice(v), base);
@@ -1375,14 +1375,15 @@ namespace polysat {
             unsigned const hi = lo + w - 1;
             if (try_get_value(r, a)) {
                 out.push_back({hi, lo, a});
-                out_just.push_back({n, r});
+                out_just.push_back(n);
             }
             lo += w;
         }
     }
 
-    void slicing::explain_fixed(euf::enode_pair const& just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
-        auto [n, r] = just;
+    void slicing::explain_fixed(euf::enode* const n, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
+        enode* const r = n->get_root();
+        SASSERT(is_value(r));
         NOT_IMPLEMENTED_YET(); // TODO: like explain_value
     }
 
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 97162a153..d2d30a6b1 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -339,8 +339,8 @@ namespace polysat {
         void collect_simple_overlaps(pvar v, pvar_vector& out);
 
         /** Collect fixed portions of the variable v */
-        void collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_pair_vector& out_just);
-        void explain_fixed(euf::enode_pair const& just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
+        void collect_fixed(pvar v, fixed_bits_vector& out, enode_vector& out_just);
+        void explain_fixed(euf::enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
 
         std::ostream& display(std::ostream& out) const;
         std::ostream& display_tree(std::ostream& out) const;
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 530d9dda4..342b53dfa 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -976,7 +976,7 @@ namespace {
 #if 0
         // TODO: wip
         fixed_bits_vector fbs;
-        euf::enode_pair_vector fbs_just;
+        euf::enode_vector fbs_just;
         s.m_slicing.collect_fixed(v, fbs, fbs_just);
 
         for (unsigned idx = fbs.size(); idx-- > 0; ) {