diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index ff5761cb2..59143e4a7 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -28,12 +28,6 @@ Example:
 
 
 TODO:
-- notify solver about equalities discovered by congruence
-    - variable equalities x = y will be handled on-demand by the viable component
-    - but whenever we derive an equality between pvar and value we must propagate the value in the solver
-        -> need a way to store and retrieve justification for this propagation (explain_equal)
-- track fixed bits along with enodes
-- implement query functions
 - About the sub-slice sharing among equivalent nodes:
   - When extracting a variable y := x[h:l], we always need to create a new slice for y.
   - Merge slices for x[h:l] with y; store as dependency 'x[h:l]' (rather than 'null_dep' as we do now).
@@ -47,24 +41,9 @@ TODO:
     - a question is how to track/handle the dependency on the assignment
 - check Algorithm 2 of "Solving Bitvectors with MCSAT"; what is the difference to what we are doing now?
 - track equalities such as x = -y ?
-
-
-
-
-Current issue:
-
-        1. mk_extract v7 := v6[63:32]
-        2. solver assigns v7 := 1
-        3. solver assigns v6 := 1 by decision
-
-        This is a conflict, because v6[63:32] = 0, v7 = v6[63:32], v7 = 1.
-
-        Solution:
-        - when finding a viable value for v6 to make a decision,
-          call slicing::collect_fixed to find already fixed bits
-        - v7 is a subslice of v6, so we find v6[63:32] = 1
-        - viable can already deal with fixed bits
-          (needs some refactoring because of how justifications are tracked)
+- on_merge could propagate values upwards:
+    if slice has value but parent has no value, then check if sub_other(parent(s)) [sibling(s)?] has a value.
+    if yes, can propagate value upwards. (add a congruence term to track deps properly?)
 
 */
 
@@ -145,13 +124,14 @@ namespace polysat {
         m_egraph.set_display_justification([&](std::ostream& out, void* dp) { display(out, dep_t::decode(dp)); });
         m_egraph.set_on_merge([&](enode* root, enode* other) { egraph_on_merge(root, other); });
         m_egraph.set_on_propagate([&](enode* lit, enode* ante) { egraph_on_propagate(lit, ante); });
+        // m_egraph.set_on_make([&](enode* n) { egraph_on_make(n); });
     }
 
-    slicing::slice_info& slicing::info(euf::enode* n) {
+    slicing::slice_info& slicing::info(enode* n) {
         return const_cast<slice_info&>(std::as_const(*this).info(n));
     }
 
-    slicing::slice_info const& slicing::info(euf::enode* n) const {
+    slicing::slice_info const& slicing::info(enode* n) const {
         SASSERT(n);
         SASSERT(!n->is_equality());
         SASSERT(m_bv->is_bv_sort(n->get_sort()));
@@ -230,6 +210,9 @@ namespace polysat {
             case trail_item::mk_concat:
                 num_replay_concat++;
                 break;
+            case trail_item::set_value_node:
+                undo_set_value_node();
+                break;
             default:
                 UNREACHABLE();
             }
@@ -267,6 +250,9 @@ namespace polysat {
                 replay_concat(ci.num_args, &m_concat_args[ci.args_idx], ci.v);
                 break;
             }
+            case trail_item::set_value_node:
+                /* do nothing */
+                break;
             default:
                 UNREACHABLE();
             }
@@ -274,6 +260,7 @@ namespace polysat {
         m_concat_trail.shrink(m_concat_trail.size() - num_replay_concat);
         m_concat_args.shrink(m_concat_trail.empty() ? 0 : m_concat_trail.back().next_args_idx());
         m_trail.shrink(target_size);
+        SASSERT(invariant());
     }
 
     void slicing::add_var(unsigned bit_width) {
@@ -300,13 +287,23 @@ namespace polysat {
         return eqn;
     }
 
+#if 0
+    void slicing::egraph_on_make(enode* n) {
+        LOG("on_make: " << e_pp(n));
+    }
+#endif
+
     slicing::enode* slicing::alloc_enode(expr* e, unsigned num_args, enode* const* args, pvar var) {
         SASSERT(!m_egraph.find(e));
-        euf::enode* n = m_egraph.mk(e, 0, num_args, args);  // NOTE: the egraph keeps a strong reference to 'e'
-        m_info.reserve(n->get_id() + 1);
-        slice_info& i = info(n);
+        // NOTE: sometimes egraph::mk already triggers a merge due to congruence.
+        //       in this case we have to make sure to allocate m_info early enough.
+        unsigned const id = e->get_id();
+        m_info.reserve(id + 1);
+        slice_info& i = m_info[id];
         i.reset();
         i.var = var;
+        enode* n = m_egraph.mk(e, 0, num_args, args);  // NOTE: the egraph keeps a strong reference to 'e'
+        LOG("alloc_enode: " << e_pp(n));
         return n;
     }
 
@@ -321,7 +318,7 @@ namespace polysat {
 
     slicing::enode* slicing::alloc_slice(unsigned width, pvar var) {
         SASSERT(width > 0);
-        app* a = m_ast.mk_fresh_const("s", m_bv->mk_sort(width), false);
+        app_ref a(m_ast.mk_fresh_const("s", m_bv->mk_sort(width), false), m_ast);
         return alloc_enode(a, 0, nullptr, var);
     }
 
@@ -391,12 +388,14 @@ namespace polysat {
         else {
             sub_hi = alloc_slice(width_hi);
             sub_lo = alloc_slice(width_lo);
-            info(sub_hi).parent = s;
-            info(sub_lo).parent = s;
         }
+        SASSERT(!parent(sub_hi));
+        SASSERT(!parent(sub_lo));
+        info(sub_hi).parent = s;
+        info(sub_lo).parent = s;
         info(s).set_cut(cut, sub_hi, sub_lo);
         m_trail.push_back(trail_item::split_core);
-        m_split_trail.push_back(s);
+        m_enode_trail.push_back(s);
         for (enode* n = s; n != nullptr; n = parent(n)) {
             pvar const v = slice2var(n);
             if (v == null_var)
@@ -419,8 +418,8 @@ namespace polysat {
     }
 
     void slicing::undo_split_core() {
-        enode* s = m_split_trail.back();
-        m_split_trail.pop_back();
+        enode* s = m_enode_trail.back();
+        m_enode_trail.pop_back();
         info(s).set_cut(null_cut, nullptr, nullptr);
     }
 
@@ -437,7 +436,6 @@ namespace polysat {
             enode* target = n->get_target();
             if (!target)
                 continue;
-            SASSERT(!is_value(n));  // values are always roots, and target always points towards the root.
             euf::justification const j = n->get_justification();
             SASSERT(j.is_external());  // cannot be a congruence since the slice wasn't split before.
             dep_t const d = dep_t::decode(j.ext<void>());
@@ -509,14 +507,32 @@ namespace polysat {
 
     slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) {
         SASSERT(0 <= val && val < rational::power_of_two(bit_width));
-        app_ref a(m_bv->mk_numeral(val, bit_width), m_ast);
-        enode* s = find_or_alloc_enode(a, 0, nullptr, null_var);
-        s->mark_interpreted();
-        SASSERT(s->interpreted());
+        sort* bv_sort = m_bv->mk_sort(bit_width);
+        func_decl_ref f(m_ast.mk_fresh_func_decl("val", nullptr, 1, &bv_sort, bv_sort, false), m_ast);
+        app_ref a(m_ast.mk_app(f, m_bv->mk_numeral(val, bit_width)), m_ast);
+        enode* s = alloc_enode(a, 0, nullptr, null_var);
+        set_value_node(s, s);
         SASSERT_EQ(get_value(s), val);
         return s;
     }
 
+    slicing::enode* slicing::mk_interpreted_value_node(enode* s) {
+        SASSERT(is_value(s));
+        // NOTE: how this is used now, the node will not yet be contained in the egraph.
+        enode* n = alloc_enode(s->get_app()->get_arg(0), 0, nullptr, null_var);
+        info(n).value_node = s;
+        n->mark_interpreted();
+        SASSERT(n->interpreted());
+        SASSERT_EQ(get_value_node(n), s);
+        return n;
+    }
+
+    bool slicing::is_value(enode* n) const {
+        SASSERT(is_app(n->get_expr()));  // we only create app nodes at the moment; if this fails just return false here.
+        app* a = n->get_app();
+        return a->get_num_args() == 1 && m_bv->is_numeral(a->get_arg(0));
+    }
+
     rational slicing::get_value(enode* s) const {
         SASSERT(is_value(s));
         rational val;
@@ -525,7 +541,10 @@ namespace polysat {
     }
 
     bool slicing::try_get_value(enode* s, rational& val) const {
-        bool const ok = m_bv->is_numeral(s->get_expr(), val);
+        app* a = s->get_app();
+        if (a->get_num_args() != 1)
+            return false;
+        bool const ok = m_bv->is_numeral(a->get_arg(0), val);
         SASSERT_EQ(ok, is_value(s));
         return ok;
     }
@@ -591,6 +610,7 @@ namespace polysat {
         SASSERT(is_conflict());
         m_egraph.begin_explain();
         if (m_disequality_conflict) {
+            LOG("Disequality conflict: " << m_disequality_conflict);
             enode* eqn = m_disequality_conflict;
             SASSERT(eqn->is_equality());
             SASSERT_EQ(eqn->value(), l_false);
@@ -654,18 +674,23 @@ namespace polysat {
         m_tmp_deps.reset();
         if (x != null_var) LOG("Variable v" << x << " with slice " << slice_pp(*this, sx));
         if (y != null_var) LOG("Variable v" << y << " with slice " << slice_pp(*this, sy));
-        SASSERT(x != null_var || y == null_var);
-        SASSERT(y != null_var || x == null_var);
+        // SASSERT(x != null_var || y == null_var);
+        // SASSERT(y != null_var || x == null_var);
 
+        // Algorithm 1 in BitvectorsMCSAT
         signed_constraint c;
         if (x == null_var) {
             /* nothing to do */
             SASSERT_EQ(y, null_var);
         }
         else if (y == null_var) {
+            SASSERT(get_value_node(sx));
+            unsigned hi, lo;
+            VERIFY(find_range_in_ancestor(sx, var2slice(x), hi, lo));
+            LOG("Variable v" << x << " has solver-value " << m_solver.get_value(x));
+            LOG("Subslice v" << x << "[" << hi << ":" << lo << "] has value " << get_value(get_value_node(sx)));
             UNREACHABLE();
             /*
-            SASSERT(is_value(sx->get_root()));
             // the egraph has derived that x (or a sub-slice thereof) must have value b that differs from the currently assigned value of x.
             // the explanation is:      lits ==> x[...] = b
             enode* const xn = var2slice(x)->get_root();
@@ -680,8 +705,8 @@ namespace polysat {
                 unsigned hi, lo;
                 VERIFY(find_range_in_ancestor(sx, var2slice(x), hi, lo));
                 LOG("Variable v" << x << " has solver-value " << m_solver.get_value(x));
-                LOG("Subslice v" << x << "[" << hi << ":" << lo << "] has value " << get_value(sx->get_root()));
-                rational const b = get_value(sx->get_root());
+                LOG("Subslice v" << x << "[" << hi << ":" << lo << "] has value " << get_value(get_value_node(sx)));
+                rational const b = get_value(get_value_node(sx));
                 // TODO: problematic case when this assertion is violated:
                 // 1. v3 := v2[0:0]
                 // 2. propagate value assignment v2 := 1 from some other constraints.
@@ -711,12 +736,16 @@ namespace polysat {
             */
         }
         else {
+            display_tree(std::cout);
+            SASSERT(y != null_var);
             SASSERT(x != y);
+            SASSERT(get_value_node(sx));
+            SASSERT(get_value_node(sy));
             unsigned x_hi, x_lo, y_hi, y_lo;
             VERIFY(find_range_in_ancestor(sx, var2slice(x), x_hi, x_lo));
             VERIFY(find_range_in_ancestor(sy, var2slice(y), y_hi, y_lo));
-            LOG("find_range_in_ancestor: v" << x << "[" << x_hi << ":" << x_lo << "] = " << slice_pp(*this, sx) << ", slice-value " << get_value(sx->get_root()));
-            LOG("find_range_in_ancestor: v" << y << "[" << y_hi << ":" << y_lo << "] = " << slice_pp(*this, sy) << ", slice-value " << get_value(sy->get_root()));
+            LOG("find_range_in_ancestor: v" << x << "[" << x_hi << ":" << x_lo << "] = " << slice_pp(*this, sx) << ", slice-value " << get_value(get_value_node(sx)));
+            LOG("find_range_in_ancestor: v" << y << "[" << y_hi << ":" << y_lo << "] = " << slice_pp(*this, sy) << ", slice-value " << get_value(get_value_node(sy)));
             if (m_solver.is_assigned(x)) {
                 rational sval = mod2k(machine_div2k(m_solver.get_value(x), x_lo), x_hi - x_lo + 1);
                 LOG("Variable v" << x << " has solver-value " << m_solver.get_value(x) << ", i.e., v" << x << "[" << x_hi << ":" << x_lo << "] = " << sval);
@@ -730,8 +759,8 @@ namespace polysat {
             // below is TODO
 
 
-            // LOG("Slice sx=" << slice_pp(*this, sx) << " has value " << get_value(sx->get_root()));
-            // LOG("Slice sy=" << slice_pp(*this, sy) << " has value " << get_value(sy->get_root()));
+            // LOG("Slice sx=" << slice_pp(*this, sx) << " has value " << get_value(get_value_node(sx)));
+            // LOG("Slice sy=" << slice_pp(*this, sy) << " has value " << get_value(get_value_node(sy)));
             // the egraph has derived that x (or a subslice of x) must be equal to y (or a subslice of y),
             // but the currently assigned values differ.
             // the explanation is:      lits ==> x[...] = y[...]
@@ -746,13 +775,13 @@ namespace polysat {
                 //      (it is also hard and probably not useful to handle otherwise)
 
                 // we handle one special case for now
-                if (sx->get_root() == var2slice(x)->get_root() && m_solver.get_value(x) != get_value(var2slice(x)->get_root())) {
-                    LOG("Variable v" << x << " has solver-value " << m_solver.get_value(x) << " and slicing-value " << get_value(var2slice(x)->get_root()));
+                if (sx->get_root() == var2slice(x)->get_root() && m_solver.get_value(x) != get_value(get_value_node(var2slice(x)))) {
+                    LOG("Variable v" << x << " has solver-value " << m_solver.get_value(x) << " and slicing-value " << get_value(get_value_node(var2slice(x))));
                     // here, the learned clause should be   y = value(y)  ==>  x = slicing-value(x)
                     signed_constraint d = m_solver.eq(m_solver.var(y), m_solver.get_value(y));
                     LOG("Premise:    " << lit_pp(m_solver, d));
                     cb.insert_eval(~d);
-                    c = m_solver.eq(m_solver.var(x), get_value(sx->get_root()));
+                    c = m_solver.eq(m_solver.var(x), get_value(get_value_node(sx)));
                 }
             }
             else {
@@ -777,6 +806,7 @@ namespace polysat {
             LOG("Conclusion: <conflict>");
         }
 
+        std::abort();
         return cb.build();
     }
 
@@ -784,11 +814,11 @@ namespace polysat {
         SASSERT(invariant());
         SASSERT(m_marked_lits.empty());
 
-        enode* r = s->get_root();
-        SASSERT(is_value(r));  // by convention, value slices are always the root; and this method may only be called if s is equivalent to a value node.
+        enode* n = get_value_node(s);
+        SASSERT(is_value(n));
 
         SASSERT(m_tmp_deps.empty());
-        explain_equal(s, r, m_tmp_deps);
+        explain_equal(s, n, m_tmp_deps);
 
         for (void* dp : m_tmp_deps) {
             dep_t const d = dep_t::decode(dp);
@@ -838,22 +868,58 @@ namespace polysat {
     }
 
     void slicing::egraph_on_merge(enode* root, enode* other) {
-        SASSERT(!is_value(other));  // by convention, interpreted nodes are always chosen as root
-        if (is_value(root)) {
+        // LOG("on_merge:\nroot " << e_pp(root) << "other " << e_pp(other));
+        if (root->interpreted())
+            return;
+        SASSERT(!other->interpreted());  // by convention, interpreted nodes are always chosen as root
+        SASSERT(root != other);
+        SASSERT_EQ(root, root->get_root());
+        SASSERT_EQ(root, other->get_root());
+
+        enode* v1 = info(root).value_node;   // root is the root
+        enode* v2 = info(other).value_node;  // 'other' was its own root before the merge
+        if (v1 && v2 && get_value(v1) != get_value(v2)) {
+            // we have a conflict. add interpreted enodes to make the egraph realize it.
+            enode* i1 = mk_interpreted_value_node(v1);
+            enode* i2 = mk_interpreted_value_node(v2);
+            m_egraph.merge(i1, v1, dep_t().encode());
+            m_egraph.merge(i2, v2, dep_t().encode());
+            SASSERT(is_conflict());
+            return;
+        }
+
+        if (v1 || v2) {
+            if (!v1) set_value_node(root, v2);
+            if (!v2) set_value_node(other, v1);
+            rational const val = get_value(v1 ? v1 : v2);
             for (enode* n : euf::enode_class(other)) {
                 pvar const v = slice2var(n);
                 if (v == null_var)
                     continue;
                 if (m_solver.is_assigned(v))
                     continue;
-                LOG("on_merge: v" << v << " := " << get_value(root));
-                m_solver.assign_propagate_by_slicing(v, get_value(root));
-                // TODO: congruence? what if all base slices of a variable are equivalent to values?
-                //          -> could track, for each variable, how many of its base slices are (not) equivalent to values. (update on split and merge)
+                LOG("on_merge: v" << v << " := " << val);
+                m_solver.assign_propagate_by_slicing(v, val);
             }
         }
     }
 
+    void slicing::set_value_node(enode* s, enode* value_node) {
+        SASSERT(!info(s).value_node);
+        SASSERT(is_value(value_node));
+        info(s).value_node = value_node;
+        if (s != value_node) {
+            m_trail.push_back(trail_item::set_value_node);
+            m_enode_trail.push_back(s);
+        }
+    }
+
+    void slicing::undo_set_value_node() {
+        enode* s = m_enode_trail.back();
+        m_enode_trail.pop_back();
+        info(s).value_node = nullptr;
+    }
+
     void slicing::egraph_on_propagate(enode* lit, enode* ante) {
         // ante may be set when symmetric equality is added by congruence
         if (ante)
@@ -882,7 +948,17 @@ namespace polysat {
     }
 
     bool slicing::egraph_merge(enode* s1, enode* s2, dep_t dep) {
+        LOG("egraph_merge: " << slice_pp(*this, s1) << " and " << slice_pp(*this, s2));
         SASSERT_EQ(width(s1), width(s2));
+        enode* v1 = get_value_node(s1);
+        enode* v2 = get_value_node(s2);
+        if (v1 && v2 && get_value(v1) == get_value(v2)) {
+            // optimization: if s1, s2 are already equivalent to the same value,
+            // then they could have been merged already and we do not need to record 'dep'.
+            // merge the value slices instead.
+            m_egraph.merge(v1, v2, dep_t().encode());
+            return !is_conflict();
+        }
         if (dep.is_value()) {
             if (is_value(s1))
                 std::swap(s1, s2);
@@ -896,6 +972,7 @@ namespace polysat {
     }
 
     bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
+        LOG("merge_base: " << slice_pp(*this, s1) << " and " << slice_pp(*this, s2));
         SASSERT(!has_sub(s1));
         SASSERT(!has_sub(s2));
         return egraph_merge(s1, s2, dep);
@@ -968,6 +1045,7 @@ namespace polysat {
     }
 
     bool slicing::merge(enode* x, enode* y, dep_t dep) {
+        LOG("merge: " << slice_pp(*this, x) << " and " << slice_pp(*this, y));
         SASSERT_EQ(width(x), width(y));
         if (!has_sub(x) && !has_sub(y))
             return merge_base(x, y, dep);
@@ -990,28 +1068,28 @@ namespace polysat {
         enode_vector& ys = m_tmp3;
         SASSERT(xs.empty());
         SASSERT(ys.empty());
+        on_scope_exit clear_vectors([&xs, &ys](){
+            xs.clear();
+            ys.clear();
+        });
         // TODO: we don't always have to collect the full base if intermediate nodes are already equal
-        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);
-        xs.clear();
-        ys.clear();
-        return result;
+        get_base(x, xs);
+        get_base(y, ys);
+        if (xs.size() != ys.size())
+            return false;
+        for (unsigned i = xs.size(); i-- > 0; )
+            if (xs[i]->get_root() != ys[i]->get_root())
+                return false;
+        return true;
     }
 
-    template <bool should_get_root>
-    void slicing::get_base_core(enode* src, enode_vector& out_base) const {
+    void slicing::get_base(enode* src, enode_vector& out_base) const {
         enode_vector& todo = m_tmp1;
         SASSERT(todo.empty());
         todo.push_back(src);
         while (!todo.empty()) {
             enode* s = todo.back();
             todo.pop_back();
-            if constexpr (should_get_root) {
-                s = s->get_root();
-            }
             if (!has_sub(s))
                 out_base.push_back(s);
             else {
@@ -1022,14 +1100,6 @@ namespace polysat {
         SASSERT(todo.empty());
     }
 
-    void slicing::get_base(enode* src, enode_vector& out_base) const {
-        get_base_core<false>(src, out_base);
-    }
-
-    void slicing::get_root_base(enode* src, enode_vector& out_base) const {
-        get_base_core<true>(src, out_base);
-    }
-
     pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_var) {
         LOG("mk_extract: src=" << slice_pp(*this, src) << " hi=" << hi << " lo=" << lo);
         enode_vector& slices = m_tmp3;
@@ -1237,7 +1307,7 @@ namespace polysat {
         }
         else {
             LOG("    store disequality v" << x << " != v" << y);
-            enode* n = find_or_alloc_disequality(sy, sx, lit);
+            enode* n = find_or_alloc_disequality(sx, sy, lit);
             if (!m_disequality_conflict && is_equal(sx, sy)) {
                 add_var_congruence_if_needed(x);
                 add_var_congruence_if_needed(y);
@@ -1396,11 +1466,11 @@ namespace polysat {
             out << "v" << v << ":";
             base.reset();
             enode* const vs = var2slice(v);
-            get_root_base(vs, base);
+            get_base(vs, base);
             for (enode* s : base)
                 display(out << " ", s);
-            if (is_value(vs->get_root()))
-                out << "    [root_value: " << get_value(vs->get_root()) << "]";
+            if (enode* vnode = get_value_node(vs))
+                out << "    [root_value: " << get_value(vnode) << "]";
             out << "\n";
         }
         return out;
@@ -1426,8 +1496,8 @@ namespace polysat {
             out << " parent=" << parent(s)->get_id();
         if (!s->is_root())
             out << " root=" << s->get_root_id();
-        if (is_value(s->get_root()))
-            out << " root_value=" << get_value(s->get_root());
+        if (enode* n = get_value_node(s))
+            out << " value=" << get_value(n);
         // if (is_proper_slice(s))
         //     out << " <slice>";
         if (is_value(s))
@@ -1448,8 +1518,11 @@ namespace polysat {
     std::ostream& slicing::display(std::ostream& out, enode* s) const {
         out << "{id:" << s->get_id();
         out << ",w:" << width(s);
+        out << ",root:" << s->get_root_id();
         if (is_value(s))
-            out << ",<value>";
+            out << ",value:" << get_value(s);
+        if (s->interpreted())
+            out << ",<interpreted>";
         if (is_concat(s))
             out << ",<concat>";
         if (is_equality(s))
@@ -1462,6 +1535,8 @@ namespace polysat {
         VERIFY(m_tmp1.empty());
         VERIFY(m_tmp2.empty());
         VERIFY(m_tmp3.empty());
+        if (is_conflict())  // if we break a loop early on conflict, we can't guarantee that all properties are satisfied
+            return true;
         for (enode* s : m_egraph.nodes()) {
             // we use equality enodes only to track disequalities
             if (s->is_equality())
@@ -1472,12 +1547,9 @@ namespace polysat {
                 VERIFY_EQ(var2slice(v)->get_root(), s->get_root());
             }
             // if slice has a value, it should be propagated to its sub-slices
-            if (is_value(s)) {
-                VERIFY(s->is_root());
-                if (has_sub(s)) {
-                    VERIFY(is_value(sub_hi(s)));
-                    VERIFY(is_value(sub_lo(s)));
-                }
+            if (get_value_node(s) && has_sub(s)) {
+                VERIFY(get_value_node(sub_hi(s)));
+                VERIFY(get_value_node(sub_lo(s)));
             }
             // a base slice is never equivalent to a congruence node
             if (is_slice(s) && !has_sub(s)) {
@@ -1491,14 +1563,18 @@ namespace polysat {
                 VERIFY(is_slice(sv));
                 VERIFY(s->num_args() >= 2);
             }
-            // properties below only matter for representatives
+            /////////////////////////////////////////////////////////////////
+            // class properties (i.e., skip non-representatives)
             if (!s->is_root())
                 continue;
+            bool const sub = has_sub(s);
             enode_vector s_base;
             get_base(s, s_base);
             for (enode* n : euf::enode_class(s)) {
                 // equivalence class only contains slices of equal length
                 VERIFY_EQ(width(s), width(n));
+                // either all nodes in the class have subslices or none do
+                SASSERT_EQ(sub, has_sub(n));
                 // bases of equivalent nodes are equivalent
                 enode_vector n_base;
                 get_base(n, n_base);
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index fda2d1e3e..0ebfb29eb 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -41,6 +41,7 @@ namespace polysat {
 
     public:
         using enode = euf::enode;
+        using enode_pair = euf::enode_pair;
         using enode_vector = euf::enode_vector;
 
     private:
@@ -81,6 +82,7 @@ namespace polysat {
         // We use the following kinds of enodes:
         // - proper slices (of variables)
         // - value slices
+        // - interpreted value nodes ... these are short-lived, and only created to immediately trigger a conflict inside the egraph
         // - virtual concat(...) expressions
         // - equalities between enodes (to track disequalities; currently not represented in slice_info)
         struct slice_info {
@@ -92,6 +94,7 @@ namespace polysat {
             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]
+            enode*      value_node = nullptr;   // the root of an equivalence class stores the value slice here, if any
 
             void reset() { *this = slice_info(); }
             bool has_sub() const { return !!sub_hi; }
@@ -103,7 +106,7 @@ namespace polysat {
         bool is_slice(enode* n) const;
 
         bool is_proper_slice(enode* n) const { return !is_value(n) && is_slice(n); }
-        bool is_value(enode* n) const { return n->interpreted(); }
+        bool is_value(enode* n) const;
         bool is_concat(enode* n) const;
         bool is_equality(enode* n) const { return n->is_equality(); }
 
@@ -148,6 +151,9 @@ namespace polysat {
 
         enode* parent(enode* s) const { return info(s).parent; }
 
+        enode* get_value_node(enode* s) const { return info(s->get_root()).value_node; }
+        void set_value_node(enode* s, enode* value_node);
+
         bool has_sub(enode* s) const { return info(s).has_sub(); }
 
         /// Upper subslice (direct child, not necessarily the representative)
@@ -159,6 +165,9 @@ namespace polysat {
         // Retrieve (or create) a slice representing the given value.
         enode* mk_value_slice(rational const& val, unsigned bit_width);
 
+        // Turn value node into unwrapped BV constant node
+        enode* mk_interpreted_value_node(enode* value_slice);
+
         rational get_value(enode* s) const;
         bool try_get_value(enode* s, rational& val) const;
 
@@ -166,13 +175,8 @@ namespace polysat {
         void split(enode* s, unsigned cut);
         void split_core(enode* s, unsigned cut);
 
-        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 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.
@@ -195,6 +199,7 @@ namespace polysat {
         /** Extract reason for x == y */
         void explain_equal(pvar x, pvar y, ptr_vector<void>& out_deps);
 
+        void egraph_on_make(enode* n);
         void egraph_on_merge(enode* root, enode* other);
         void egraph_on_propagate(enode* lit, enode* ante);
 
@@ -233,18 +238,19 @@ namespace polysat {
         using extract_args_hash = obj_hash<extract_args>;
         using extract_map = map<extract_args, pvar, extract_args_hash, extract_args_eq>;
         extract_map m_extract_dedup;
-
-        bool is_extract(pvar v) const;
-        bool is_extract(pvar v, pvar& out_src, pvar& out_hi, pvar& out_lo) const;
+        // svector<extract_args> m_extract_origin;  // pvar -> extract_args
+        // TODO: add 'm_extract_origin' (pvar -> extract_args)? 1. for dependency tracking when sharing subslice trees; 2. for easily checking if a variable is an extraction of another; 3. also makes the replay easier
+        // bool is_extract(pvar v) const { return m_extract_origin[v].src != null_var; }
 
         enum class trail_item : std::uint8_t {
             add_var,
             split_core,
             mk_extract,
             mk_concat,
+            set_value_node,
         };
         svector<trail_item> m_trail;
-        enode_vector        m_split_trail;
+        enode_vector        m_enode_trail;
         svector<extract_args> m_extract_trail;
         unsigned_vector     m_scopes;
 
@@ -260,6 +266,7 @@ namespace polysat {
         void undo_add_var();
         void undo_split_core();
         void undo_mk_extract();
+        void undo_set_value_node();
 
         mutable enode_vector m_tmp1;
         mutable enode_vector m_tmp2;
@@ -305,6 +312,8 @@ namespace polysat {
         };
         friend std::ostream& operator<<(std::ostream& out, dep_pp const& d) { return d.display(out); }
 
+        euf::egraph::e_pp e_pp(enode* n) const { return euf::egraph::e_pp(m_egraph, n); }
+
     public:
         slicing(solver& s);
 
diff --git a/src/test/slicing.cpp b/src/test/slicing.cpp
index 92d733127..a54f647ac 100644
--- a/src/test/slicing.cpp
+++ b/src/test/slicing.cpp
@@ -29,7 +29,9 @@ namespace polysat {
 
     class scoped_solver_slicing : public solver_scope_slicing, public solver {
     public:
-        scoped_solver_slicing(): solver(lim, pars) {}
+        scoped_solver_slicing(): solver(lim, pars) {
+            set_log_enabled(false);
+        }
         slicing& sl() { return m_slicing; }
     };
 
@@ -75,12 +77,14 @@ namespace polysat {
             VERIFY(sl.merge(y_5_0, sl.var2slice(b), sat::literal(2)));
             std::cout << sl << "\n";
 
+/*
             slicing::enode_vector x_base;
             sl.get_root_base(sl.var2slice(x), x_base);
             slicing::enode_vector y_base;
             sl.get_root_base(sl.var2slice(y), y_base);
             VERIFY(sl.merge(x_base, y_base, sat::literal(3)));
             std::cout << sl << "\n";
+*/
 
             sl.display_tree(std::cout);
             VERIFY(sl.invariant());
@@ -212,6 +216,11 @@ namespace polysat {
         // x[3:0] = z
         // y = 0b1001
         // z = 0b0111
+        //
+        // x:  xxxxxx
+        // y:  1001
+        // z:    0111
+        // (no conflict)
         static void test5() {
             std::cout << __func__ << "\n";
             scoped_solver_slicing s;
@@ -232,6 +241,43 @@ namespace polysat {
             VERIFY(sl.merge(sl.var2slice(z), seven, sat::literal(107)));
             std::cout << "v" << z << " = 7\n" << sl << "\n";
 
+            VERIFY(!sl.is_conflict());
+
+            sl.display_tree(std::cout);
+            VERIFY(sl.invariant());
+        }
+
+        // x[5:2] = y
+        // x[3:0] = z
+        // y = 0b1001
+        // z = 0b1011
+        //
+        // x:  xxxxxx
+        // y:  1001
+        // z:    1011
+        // (conflict)
+        static void test5b() {
+            std::cout << __func__ << "\n";
+            scoped_solver_slicing s;
+            slicing& sl = s.sl();
+            pvar x = s.add_var(6);
+            std::cout << sl << "\n";
+
+            pvar y = sl.mk_extract(x, 5, 2);
+            std::cout << "v" << y << " := v" << x << "[5:2]\n" << sl << "\n";
+            pvar z = sl.mk_extract(x, 3, 0);
+            std::cout << "v" << z << " := v" << x << "[3:0]\n" << sl << "\n";
+
+            slicing::enode* nine = sl.mk_value_slice(rational(9), 4);
+            VERIFY(sl.merge(sl.var2slice(y), nine, sat::literal(109)));
+            std::cout << "v" << y << " = 9\n" << sl << "\n";
+
+            slicing::enode* eleven = sl.mk_value_slice(rational(11), 4);
+            VERIFY(!sl.merge(sl.var2slice(z), eleven, sat::literal(107)));
+            std::cout << "v" << z << " = 11\n" << sl << "\n";
+
+            VERIFY(sl.is_conflict());
+
             sl.display_tree(std::cout);
             VERIFY(sl.invariant());
         }
@@ -264,7 +310,6 @@ namespace polysat {
         // in various permutations
         static void test7() {
             std::cout << __func__ << "\n";
-            scoped_set_log_enabled _logging(false);
             scoped_solver_slicing s;
             slicing& sl = s.sl();
             pdd x = s.var(s.add_var(8));
@@ -374,6 +419,68 @@ namespace polysat {
             VERIFY(sl.invariant());
         }
 
+        // x == 7
+        // y == 7
+        static void test11() {
+            std::cout << __func__ << "\n";
+            scoped_solver_slicing s;
+            slicing& sl = s.sl();
+            pvar x = s.add_var(8);
+            sl.add_constraint(s.eq(s.var(x), 7));
+            pvar a = sl.mk_extract(x, 7, 6);
+            pvar b = sl.mk_extract(x, 3, 0);
+            sl.display_tree(std::cout);
+
+            pvar y = s.add_var(8);
+            pvar c = sl.mk_extract(y, 7, 6);
+            pvar d = sl.mk_extract(y, 1, 0);
+            sl.display_tree(std::cout);
+
+            sl.add_constraint(s.eq(s.var(y), 7));
+            sl.display_tree(std::cout);
+        }
+
+
+
+        // x == 0
+        // x != y
+        // y <= 1
+        // y[0:0] = z
+        // z == w
+        // w == 0
+        static void test12() {
+            std::cout << __func__ << "\n";
+            // TODO
+            scoped_solver_slicing s;
+            slicing& sl = s.sl();
+        }
+
+
+        // mk_extract y := x[63:32]
+        // a * x = 123
+        // b * y = 456
+        // a = 1, propagates x = 123 (by constraint)
+        // b = 1, propagates y = 456 (by constraint), propagates x = 0 (by slicing)
+        // Conflict in slicing.
+        static void test13() {
+            std::cout << __func__ << "\n";
+            scoped_solver_slicing s;
+            slicing& sl = s.sl();
+            pvar x = s.add_var(64);
+            pvar y = sl.mk_extract(x, 63, 32);
+            pvar a = s.add_var(64);
+            pvar b = s.add_var(32);
+            sl.add_constraint(s.eq(s.var(a)*s.var(x), 123));  // NOTE: this does nothing inside slicing atm.
+            sl.add_constraint(s.eq(s.var(b)*s.var(y), 456));
+            sl.add_value(a, 1);
+            sl.add_value(x, 123);
+            sl.add_value(b, 1);
+            sl.add_value(y, 456);
+            VERIFY(sl.is_conflict());
+            sl.display_tree(std::cout);
+            VERIFY(sl.invariant());
+        }
+
     };  // test_slicing
 
 }  // namespace polysat
@@ -386,10 +493,13 @@ void tst_slicing() {
     test_slicing::test3();
     test_slicing::test4();
     test_slicing::test5();
+    test_slicing::test5b();
     test_slicing::test6();
     test_slicing::test7();
     test_slicing::test8();
     test_slicing::test9();
     test_slicing::test10();
+    test_slicing::test11();
+    test_slicing::test13();
     std::cout << "ok\n";
 }