diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index 4a078e9ef..6636ff92f 100644
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@@ -69,7 +69,7 @@ The formal properties of saturation have to be established.
 - Saturation does not complete with respect to associativity.
 Instead the claim is along the lines that the resulting E-graph can be used as a canonizer.
 If given a set of equations E that are saturated, and terms t1, t2 that are 
-both simplified with respect to left-associativity of concatentation, and t1, t2 belong to the E-graph,
+both simplified with respect to left-associativity of concatenation, and t1, t2 belong to the E-graph,
 then t1 = t2 iff t1 ~ t2 in the E-graph.
 
 TODO: Is saturation for (7) overkill for the purpose of canonization?
@@ -451,6 +451,7 @@ namespace euf {
                 }
                 for (auto p : euf::enode_parents(sib)) {
                     if (bv.is_extract(p->get_expr(), lo, hi, e)) {
+                        // p = sib[hi:lo]
                         SASSERT(g.find(e)->get_root() == n->get_root());
                         m_todo.push_back({ p, offset + lo });
                     }
@@ -505,7 +506,7 @@ namespace euf {
             std::swap(a, b);
         SASSERT(width(a) >= width(b));
         svector<std::tuple<enode*, enode*, unsigned>> just;
-        m_jtodo.push_back({ a, 0, UINT_MAX });
+        m_jtodo.push_back({ a, 0, UINT_MAX });  // enode, offset, idx into just
         unsigned lo, hi;
         expr* e;
 
@@ -555,7 +556,6 @@ namespace euf {
                     }
                 }
             }
-
         }
         IF_VERBOSE(0,
             g.display(verbose_stream());
diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h
index 126bba541..87c54a8dc 100644
--- a/src/sat/smt/polysat/types.h
+++ b/src/sat/smt/polysat/types.h
@@ -52,6 +52,8 @@ namespace polysat {
         unsigned end() const { return offset + length; }
     };
 
+    // parent[offset+length-1:offset] ~ value
+    // child ~ value, if child != null_var
     struct fixed_claim : public fixed_slice {
         pvar parent;
         fixed_claim() = default;
@@ -66,7 +68,7 @@ namespace polysat {
         offset_slice(pvar child, unsigned offset) : child(child), offset(offset) {}
     };
 
-    // parent[X:offset] = child
+    // parent[X:offset] ~ child
     // where X = offset + size(child) - 1
     struct offset_claim : public offset_slice {
         pvar parent;
@@ -137,29 +139,29 @@ namespace polysat {
 
     using fixed_bits_vector = vector<fixed_slice>;
 
-    struct fixed_slice_extra : public fixed_slice {
-        // pvar child;
-        // unsigned offset = 0;
-        // unsigned length = 0;
-        // rational value;
-        unsigned level = 0;  // level when sub-slice was fixed to value
-        dependency dep = null_dependency;
-        fixed_slice_extra() = default;
-        fixed_slice_extra(pvar child, rational value, unsigned offset, unsigned length, unsigned level, dependency dep) :
-            fixed_slice(child, std::move(value), offset, length), level(level), dep(std::move(dep)) {}
-    };
-    using fixed_slice_extra_vector = vector<fixed_slice_extra>;
+    // struct fixed_slice_extra : public fixed_slice {
+    //     // pvar child;
+    //     // unsigned offset = 0;
+    //     // unsigned length = 0;
+    //     // rational value;
+    //     unsigned level = 0;  // level when sub-slice was fixed to value
+    //     dependency dep = null_dependency;
+    //     fixed_slice_extra() = default;
+    //     fixed_slice_extra(pvar child, rational value, unsigned offset, unsigned length, unsigned level, dependency dep) :
+    //         fixed_slice(child, std::move(value), offset, length), level(level), dep(std::move(dep)) {}
+    // };
+    // using fixed_slice_extra_vector = vector<fixed_slice_extra>;
 
-    struct offset_slice_extra : public offset_slice {
-        // pvar child;
-        // unsigned offset;
-        unsigned level = 0;                 // level when child was fixed to value
-        dependency dep = null_dependency;   // justification for fixed value
-        rational value;                     // fixed value of child
-        offset_slice_extra() = default;
-        offset_slice_extra(pvar child, unsigned offset, unsigned level, dependency dep, rational value) : offset_slice(child, offset), level(level), dep(std::move(dep)), value(std::move(value)) {}
-    };
-    using offset_slice_extra_vector = vector<offset_slice_extra>;
+    // struct offset_slice_extra : public offset_slice {
+    //     // pvar child;
+    //     // unsigned offset;
+    //     unsigned level = 0;                 // level when child was fixed to value
+    //     dependency dep = null_dependency;   // justification for fixed value
+    //     rational value;                     // fixed value of child
+    //     offset_slice_extra() = default;
+    //     offset_slice_extra(pvar child, unsigned offset, unsigned level, dependency dep, rational value) : offset_slice(child, offset), level(level), dep(std::move(dep)), value(std::move(value)) {}
+    // };
+    // using offset_slice_extra_vector = vector<offset_slice_extra>;
 
 
     using dependency_vector = vector<dependency>;
@@ -192,7 +194,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 void get_fixed_sub_slices(pvar v, fixed_bits_vector& fixed) = 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/viable.cpp b/src/sat/smt/polysat/viable.cpp
index d0710c032..fef2fc307 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -686,22 +686,48 @@ namespace polysat {
         // verbose_stream() << "m_overlaps " << m_overlaps << "\n";
         m_fixed_bits.display(verbose_stream() << "fixed: ") << "\n";
 
-        // TODO: each of subslices corresponds to one in fixed, but may occur with different pvars
+        // TODO: each of subslices corresponds to one in fixed, but may occur with different pvars.
         //       for each offset/length with pvar we need to do the projection only once.
-        fixed_slice_extra_vector fixed;
-        offset_slice_extra_vector subslices;
-        c.s.get_fixed_sub_slices(m_var, fixed, subslices);   // TODO: move into m_fixed bits?
+        //       although, the max admissible level of fixed slices depends on the child pvar under consideration, so we may not get the optimal interval anymore?
+        //       (pvars on the same slice only differ by level. the fixed value is the same for all. so we can limit by the max level of pvars and then the projection will work for at least one.)
+        fixed_bits_vector fixed;
+        c.s.get_fixed_sub_slices(m_var, fixed);   // TODO: move into m_fixed bits?
 
-        TRACE("bv", c.display(tout));
+        bool has_pvar = any_of(fixed, [](fixed_slice const& f) { return f.child != null_var; });
 
         // this case occurs if e-graph merges e.g. nodes "x - 2" and "3";
         // polysat will see assignment "x = 5" but no fixed bits
-        if (subslices.empty())
+        if (!has_pvar)
             return l_undef;
 
-        unsigned max_level = 0;
-        for (auto const& slice : subslices)
-            max_level = std::max(max_level, slice.level);
+        // level when subslice of m_var became fixed
+        unsigned_vector fixed_levels;
+        for (auto const& f : fixed) {
+            dependency dep = fixed_claim(m_var, null_var, f.value, f.offset, f.length);
+            unsigned level = c.s.level(dep);
+            fixed_levels.push_back(level);
+        }
+
+        // level when target pvars became fixed
+        unsigned_vector pvar_levels;
+        for (auto const& f : fixed) {
+            unsigned level = UINT_MAX;
+            if (f.child != null_var) {
+                dependency dep = fixed_claim(f.child, null_var, f.value, 0, f.length);
+                level = c.s.level(dep);
+            }
+            pvar_levels.push_back(level);
+        }
+
+        TRACE("bv", c.display(tout));
+
+        unsigned_vector order;
+        for (unsigned i = 0; i < fixed.size(); ++i) {
+            fixed_slice const& f = fixed[i];
+            if (f.child == null_var)
+                continue;
+            order.push_back(i);
+        }
 
         // order by:
         // - level descending
@@ -709,22 +735,33 @@ namespace polysat {
         //     not always: e.g., could assign slice at level 5 but merge makes it a sub-slice only at level 10.
         //     (seems to work by not only considering max-level sub-slices.)
         // - size ascending
-        //     e.g., prefers constant 'c' if we have pvars for both 'c' and 'concat(c,...)'
-        std::sort(subslices.begin(), subslices.end(), [&](auto const& a, auto const& b) -> bool {
-            return a.level > b.level
-                || (a.level == b.level && c.size(a.child) < c.size(b.child));
+        //     e.g., prefers 'c' if we have pvars for both 'c' and 'concat(c,...)'
+        std::sort(order.begin(), order.end(), [&](auto const& i1, auto const& i2) -> bool {
+            unsigned lvl1 = pvar_levels[i1];
+            unsigned lvl2 = pvar_levels[i2];
+            pvar v1 = fixed[i1].child;
+            pvar v2 = fixed[i2].child;
+            return lvl1 > lvl2
+                || (lvl1 == lvl2 && c.size(v1) < c.size(v2));
         });
 
-        for (auto const& slice : subslices)
-            if (auto r = propagate_from_containing_slice(e, value, e_deps, fixed, slice); r != l_undef)
+        for (auto const& i : order) {
+            auto const& slice = fixed[i];
+            unsigned const slice_level = pvar_levels[i];
+            SASSERT(slice.child != null_var);
+            lbool r = propagate_from_containing_slice(e, value, e_deps, fixed, fixed_levels, slice, slice_level);
+            if (r != l_undef)
                 return r;
+        }
         return l_undef;
     }
 
-    lbool viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_slice_extra_vector const& fixed, offset_slice_extra const& slice) {
-        pvar w = slice.child;
-        unsigned offset = slice.offset;
-        unsigned w_level = slice.level;  // level where value of w was fixed
+    lbool viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_bits_vector const& fixed, unsigned_vector const& fixed_levels, fixed_slice const& slice, unsigned slice_level) {
+        pvar const w = slice.child;
+        unsigned const offset = slice.offset;
+        unsigned const w_level = slice_level;  // level where value of w was fixed
+        SASSERT(w != null_var);
+        SASSERT_EQ(c.size(w), slice.length);
         if (w == m_var)
             return l_undef;
         if (w == e->var)
@@ -755,7 +792,7 @@ namespace polysat {
         if (offset >= v_sz)
             return l_undef;
 
-        unsigned const w_sz = c.size(w);
+        unsigned const w_sz = slice.length;
         unsigned const z_sz = offset;
         unsigned const y_sz = std::min(w_sz, v_sz - z_sz);
         unsigned const x_sz = v_sz - y_sz - z_sz;
@@ -783,13 +820,14 @@ namespace polysat {
         while (remaining_x_sz > 0 && !ivl.is_empty() && !ivl.is_full()) {
             unsigned remaining_x_end = remaining_x_sz + x_off;
             // find next fixed slice (prefer lower level)
-        // sort fixed claims by bound (upper: decreasing, lower: increasing), then by merge-level (prefer lower merge level), ignore merge level higher than var? (or just max?)
-        // note that we might choose multiple overlapping ones, if they allow to make more progress?
-            fixed_slice_extra best;
+            fixed_slice best;
             unsigned best_end = 0;
+            unsigned best_level = UINT_MAX;
             SASSERT(best_end < x_off);  // because y_sz != 0
-            for (auto const& f : fixed) {
-                if (f.level >= w_level)
+            for (unsigned i = 0; i < fixed.size(); ++i) {
+                auto const& f = fixed[i];
+                unsigned const f_level = fixed_levels[i];
+                if (f_level >= w_level)
                     continue;
                 // ??????xxxxxxxyyyyyyzzzz
                 //  1111            not useful at this point
@@ -803,9 +841,9 @@ namespace polysat {
                     continue;
                 unsigned const f_end = std::min(remaining_x_end, f.end());  // for comparison, values beyond the current range don't matter
                 if (f_end > best_end)
-                    best = f, best_end = f_end;
-                else if (f_end == best_end && f.level < best.level)
-                    best = f, best_end = f_end;
+                    best = f, best_end = f_end, best_level = f_level;
+                else if (f_end == best_end && f_level < best_level)
+                    best = f, best_end = f_end, best_level = f_level;
             }
 
             if (best_end < remaining_x_end) {
@@ -836,7 +874,8 @@ namespace polysat {
                 value = mod2k(value, a);
 
                 ivl = chop_off_upper(ivl, a, b, &value);
-                deps.push_back(best.dep);  // justification for the fixed value
+                dependency best_dep = fixed_claim(m_var, null_var, best.value, best.offset, best.length);
+                deps.push_back(best_dep);  // justification for the fixed value
                 remaining_x_sz -= a;
                 remaining_x_end -= a;
 
@@ -856,10 +895,13 @@ namespace polysat {
             SASSERT(remaining_x_sz == 0);
             unsigned remaining_z_off = z_sz - remaining_z_sz;
             // find next fixed slice (prefer lower level)
-            fixed_slice_extra best;
+            fixed_slice best;
             unsigned best_off = z_sz;
-            for (auto const& f : fixed) {
-                if (f.level >= w_level)
+            unsigned best_level = UINT_MAX;
+            for (unsigned i = 0; i < fixed.size(); ++i) {
+                auto const& f = fixed[i];
+                unsigned const f_level = fixed_levels[i];
+                if (f_level >= w_level)
                     continue;
                 // ?????????????yyyyyyzzzzz???
                 //            1111              not useful at this point
@@ -872,9 +914,9 @@ namespace polysat {
                     continue;
                 unsigned const f_off = std::max(remaining_z_off, f.offset);  // for comparison, values beyond the current range don't matter
                 if (f_off < best_off)
-                    best = f, best_off = f_off;
-                else if (f_off == best_off && f.level < best.level)
-                    best = f, best_off = f_off;
+                    best = f, best_off = f_off, best_level = f_level;
+                else if (f_off == best_off && f_level < best_level)
+                    best = f, best_off = f_off, best_level = f_level;
             }
 
             if (best_off > remaining_z_off) {
@@ -903,7 +945,8 @@ namespace polysat {
                 value = mod2k(value, b);
 
                 ivl = chop_off_lower(ivl, a, b, &value);
-                deps.push_back(best.dep);  // justification for the fixed value
+                dependency best_dep = fixed_claim(m_var, null_var, best.value, best.offset, best.length);
+                deps.push_back(best_dep);  // justification for the fixed value
                 remaining_z_sz -= b;
                 remaining_z_off += b;
 
@@ -918,11 +961,15 @@ namespace polysat {
             return l_undef;
 
         IF_VERBOSE(3, {
-            verbose_stream() << "=>  v" << w << "[" << y_sz << "] not in " << ivl << "\n";
+            verbose_stream() << "=> " << ivl << "\n";
         });
 
         deps.append(e_deps);  // explains e
-        deps.push_back(offset_claim{m_var, slice});  // explains m_var[...] = w
+        deps.push_back(offset_claim{m_var, offset_slice{w, slice.offset}});  // explains m_var[...] = w
+        // deps.push_back(offset_claim{m_var, slice});  // explains m_var[...] = w
+
+        // TODO: try first the most general projection (without assuming fixed slices; purpose: get lemma with less dependencies)
+        // TODO: for each fixed slice with multiple pvars, do the projection only once?
 
         if (ivl.is_full()) {
             // deps is a conflict
@@ -935,14 +982,18 @@ namespace polysat {
             signed_constraint sc = ~cs.ult(w_shift * (c.var(w) - ivl.lo()), w_shift * (ivl.hi() - ivl.lo()));
             dependency d = c.propagate(sc, deps, "propagate from containing slice");
 
-            verbose_stream() << "v" << w << " value " << slice.value << "\n";
-            verbose_stream() << "v" << w << " value-dep " << slice.dep << "\n";
+            // verbose_stream() << "v" << w << " value " << slice.value << "\n";
+            // verbose_stream() << "v" << w << " value-dep " << slice.dep << "\n";
 
             if (ivl.contains(slice.value)) {
+                IF_VERBOSE(3, {
+                    verbose_stream() << "=>  v" << w << "[" << y_sz << "] not in " << ivl << "\n";
+                });
                 // the conflict is projected interval + fixed value
                 deps.reset();
                 deps.push_back(d);
-                deps.push_back(slice.dep);
+                deps.push_back(fixed_claim(w, null_var, slice.value, 0, w_sz));
+                // deps.push_back(slice.dep);
                 return l_true;
             }
             else {
diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h
index 4cff7f195..5a9883059 100644
--- a/src/sat/smt/polysat/viable.h
+++ b/src/sat/smt/polysat/viable.h
@@ -116,7 +116,7 @@ namespace polysat {
         bool intersect(pvar v, entry* e);
 
         lbool propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps);
-        lbool propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_slice_extra_vector const& fixed, offset_slice_extra const& slice);
+        lbool propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_bits_vector const& fixed, unsigned_vector const& fixed_levels, fixed_slice const& slice, unsigned slice_level);
         dependency_vector m_containing_slice_deps;
 
         static r_interval chop_off_upper(r_interval const& i, unsigned Ny, unsigned Nz, rational const* y_fixed_value = nullptr);
diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp
index cd48db612..3c20c79aa 100644
--- a/src/sat/smt/polysat_egraph.cpp
+++ b/src/sat/smt/polysat_egraph.cpp
@@ -125,24 +125,23 @@ namespace polysat {
 
     // 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& pvars) {
+    void solver::get_fixed_sub_slices(pvar pv, fixed_bits_vector& fixed) {
         #define GET_FIXED_SUB_SLICES_DISPLAY 1
         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)
+            if (w == euf::null_theory_var) {
+                verbose_stream() << "SKIPPING: " << ctx.bpp(n) << "\n";
                 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);  // TODO: WRONG -- n is not actually guaranteed to be the subslice of pv
-
             euf::theory_var u = n->get_th_var(get_id());
-            // dependency dep = (u == euf::null_theory_var || u == w) ? dependency::axiom() : dependency(u, w);   // TODO: probably need an enode_pair instead?
-            // dependency dep = dependency(n, r);
+
             dependency dep = fixed_claim(pv, null_var, value, offset, length);
 
 #if GET_FIXED_SUB_SLICES_DISPLAY
@@ -151,11 +150,28 @@ namespace polysat {
             verbose_stream() << "  tv " << u;
             if (u != euf::null_theory_var)
                 verbose_stream() << " := " << m_var2pdd[u];
-            verbose_stream() << "  merge-level " << level;
+            // verbose_stream() << "  merge-level " << level;
             verbose_stream() << "\n";
 #endif
 
-            fixed.push_back(fixed_slice_extra(null_var, value, offset, length, level, dep));
+            // fixed.push_back(fixed_slice_extra(null_var, value, offset, length, level, dep));
+
+            // verbose_stream() << "     n: " << n << "    " << ctx.bpp(n) << "    tv" << u << "\n";
+            // verbose_stream() << "     r: " << r << "    " << ctx.bpp(r) << "    tv" << w << "\n";
+            // verbose_stream() << "     dep: " << dep << "\n";
+            // sat::literal_vector ante;
+            // ctx.get_eq_antecedents(n, r, ante);
+            // // verbose_stream() << "     ante1: " << ante << "\n";
+            // if (u != euf::null_theory_var) {
+            //     sat::literal_vector ante2;
+            //     ctx.get_eq_antecedents(var2enode(u), var2enode(w), ante2);
+            //     // verbose_stream() << "     ante2: " << ante2 << "\n";
+            //     std::sort(ante.begin(), ante.end());
+            //     std::sort(ante2.begin(), ante2.end());
+            //     VERIFY_EQ(ante, ante2);
+            // }
+
+            bool found_pvar = false;
 
             for (euf::enode* sib : euf::enode_class(n)) {
                 euf::theory_var s = sib->get_th_var(get_id());
@@ -164,21 +180,28 @@ namespace polysat {
                 auto const& p = m_var2pdd[s];
                 if (!p.is_var())
                     continue;
-                unsigned p_level = merge_level(sib, r);
+                // unsigned p_level = merge_level(sib, r);  // this is ok
 #if GET_FIXED_SUB_SLICES_DISPLAY
                 verbose_stream() << "        pvar " << p;
                 verbose_stream() << "  node " << ctx.bpp(sib);
                 verbose_stream() << "  tv " << s;
-                verbose_stream() << "  merge-level " << p_level;
+                // verbose_stream() << "  merge-level " << p_level;
                 verbose_stream() << "  assigned? " << m_core.get_assignment().contains(p.var());
                 if (m_core.get_assignment().contains(p.var()))
                     verbose_stream() << "  value " << m_core.get_assignment().value(p.var());
                 verbose_stream() << "\n";
 #endif
-                dependency d = dependency(r, sib);
-                pvars.push_back(offset_slice_extra(p.var(), offset, p_level, d, value));
+                // dependency d = dependency(r, sib);
+                // // dependency d = fixed_claim(pv, p.var(), value, offset, length);
+                // pvars.push_back(offset_slice_extra(p.var(), offset, p_level, d, value));
+
+                found_pvar = true;
+                fixed.push_back(fixed_slice(p.var(), value, offset, length));
             }
 
+            if (!found_pvar)
+                fixed.push_back(fixed_slice(null_var, value, offset, length));
+
             return true;
         };
 #if GET_FIXED_SUB_SLICES_DISPLAY
@@ -203,7 +226,7 @@ namespace polysat {
         expr_ref val(bv.mk_numeral(slice.value, slice.length), m);
         euf::enode* b = ctx.get_egraph().find(val);
         if (!b) {
-            verbose_stream() << v << " " << val << "\n";
+            verbose_stream() << "explain_fixed: tv" << v << " " << val << "\n";
             ctx.get_egraph().display(verbose_stream());
         }
 
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 3e9d47e72..5600e6590 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -137,7 +137,7 @@ 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())
             ;
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 1bfeb4f18..5ae5782e0 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -225,7 +225,7 @@ 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;
-        void get_fixed_sub_slices(pvar v, fixed_slice_extra_vector& fixed_bits, offset_slice_extra_vector& subslices) override;
+        void get_fixed_sub_slices(pvar v, fixed_bits_vector& fixed) 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;