diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h
index c8a8a386a..647e1711e 100644
--- a/src/sat/smt/polysat/types.h
+++ b/src/sat/smt/polysat/types.h
@@ -166,6 +166,7 @@ namespace polysat {
         virtual void get_bitvector_sub_slices(pvar v, offset_slices& out) = 0;
         virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0;
         virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice) = 0;
+        virtual void get_fixed_sub_slices(pvar v, fixed_slice_extra_vector& fixed_slice, offset_slice_extra_vector& subslices) = 0;
         virtual pdd  mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) = 0;
         virtual pdd mk_zero_extend(unsigned sz, pdd const& p) = 0;
         virtual unsigned level(dependency const& d) = 0;
diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp
index f55d25088..3c2f8da17 100644
--- a/src/sat/smt/polysat_egraph.cpp
+++ b/src/sat/smt/polysat_egraph.cpp
@@ -122,6 +122,60 @@ namespace polysat {
         m_bv_plugin->sub_slices(b, consume_slice);
         m_bv_plugin->super_slices(b, consume_slice);
     }
+
+    // walk the e-graph to retrieve fixed sub-slices along with justifications,
+    // as well as pvars that correspond to these sub-slices.
+    void solver::get_fixed_sub_slices(pvar pv, fixed_slice_extra_vector& fixed, offset_slice_extra_vector& subslices) {
+        auto consume_slice = [&](euf::enode* n, unsigned offset) -> bool {
+            euf::enode* r = n->get_root();
+            if (!r->interpreted())
+                return true;
+            euf::theory_var w = r->get_th_var(get_id());
+            if (w == euf::null_theory_var)
+                return true;
+            unsigned length = bv.get_bv_size(r->get_expr());
+            rational value;
+            VERIFY(bv.is_numeral(r->get_expr(), value));
+
+            unsigned level = merge_level(n, r);
+
+            euf::theory_var u = n->get_th_var(get_id());
+            dependency dep = (u == euf::null_theory_var) ? dependency::axiom() : dependency(u, w);   // TODO: probably need an enode_pair instead?
+
+#if 0
+            verbose_stream() << "    " << value << "[" << length << "]@" << offset;
+            verbose_stream() << "  node " << ctx.bpp(n);
+            verbose_stream() << "  tv " << u;
+            if (u != euf::null_theory_var)
+                verbose_stream() << " := " << m_var2pdd[u];
+            verbose_stream() << "  merge-level " << level;
+            // verbose_stream() << "  just " << n->get_justification();
+            verbose_stream() << "\n";
+            fixed.push_back(fixed_slice_extra(value, offset, length, level, dep));
+#endif
+
+            for (euf::enode* sib : euf::enode_class(n)) {
+                euf::theory_var s = sib->get_th_var(get_id());
+                if (s == euf::null_theory_var)
+                    continue;
+                auto const& p = m_var2pdd[s];
+                if (!p.is_var())
+                    continue;
+#if 0
+                verbose_stream() << "        pvar " << p;
+                verbose_stream() << "  node " << ctx.bpp(sib);
+                verbose_stream() << "  tv " << s;
+                verbose_stream() << "  merge-level " << merge_level(sib, r);
+                verbose_stream() << "\n";
+#endif
+                subslices.push_back(offset_slice_extra(p.var(), offset, merge_level(sib, r)));
+            }
+
+            return true;
+        };
+        theory_var v = m_pddvar2var[pv];
+        m_bv_plugin->sub_slices(var2enode(v), consume_slice);
+    }
     
     void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function<void(euf::enode*, euf::enode*)> const& consume_eq) {
         euf::theory_var v = m_pddvar2var[pv];
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 321b807fd..3eba74a82 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -225,10 +225,10 @@ namespace polysat {
         void get_bitvector_super_slices(pvar v, offset_slices& out) override;
         void get_bitvector_suffixes(pvar v, offset_slices& out) override;
         void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) override;
-        pdd  mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) override;
+        void get_fixed_sub_slices(pvar v, fixed_slice_extra_vector& fixed_bits, offset_slice_extra_vector& subslices) override;
+        pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) override;
         pdd mk_zero_extend(unsigned sz, pdd const& p) override;
         unsigned level(dependency const& d) override;
-        dependency explain_slice(pvar v, pvar w, unsigned offset);
 
         bool add_axiom(char const* name, constraint_or_dependency_list const& clause, bool redundant) {
             return add_axiom(name, clause.begin(), clause.end(), redundant);