diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index f3bc8168c..7fc6478b4 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -42,9 +42,10 @@ namespace polysat {
     }
 
     void slicing::add_var(unsigned bit_width) {
-        // pvar const v = m_var2slice.size();
+        pvar const v = m_var2slice.size();
         slice const s = alloc_slice();
         m_slice_width[s] = bit_width;
+        m_slice2var[s] = v;
         m_var2slice.push_back(s);
     }
 
@@ -60,6 +61,7 @@ namespace polysat {
         m_find.push_back(s);
         m_size.push_back(1);
         m_next.push_back(s);
+        m_slice2var.push_back(null_var);
         m_trail.push_back(trail_item::alloc_slice);
         return s;
     }
@@ -71,6 +73,7 @@ namespace polysat {
         m_find.pop_back();
         m_size.pop_back();
         m_next.pop_back();
+        m_slice2var.pop_back();
     }
 
     slicing::slice slicing::find_sub_hi(slice parent) const {
@@ -128,6 +131,12 @@ namespace polysat {
         m_find[r1] = r2;
         m_size[r2] += m_size[r1];
         std::swap(m_next[r1], m_next[r2]);
+        if (m_slice2var[r2] == null_var)
+            m_slice2var[r2] = m_slice2var[r1];
+        else {
+            // otherwise the classes should have been merged already
+            SASSERT(m_slice2var[r2] != m_slice2var[r1]);
+        }
         m_trail.push_back(trail_item::merge_class);
         m_merge_trail.push_back(r1);
     }
@@ -140,6 +149,8 @@ namespace polysat {
         m_find[r1] = r1;
         m_size[r2] -= m_size[r1];
         std::swap(m_next[r1], m_next[r2]);
+        if (m_slice2var[r2] == m_slice2var[r1])
+            m_slice2var[r2] = null_var;
     }
 
     void slicing::merge(slice_vector& xs, slice_vector& ys) {
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 330015728..b81ee9579 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -75,22 +75,24 @@ namespace polysat {
         static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max();
 
         // number of bits in the slice
-        unsigned_vector     m_slice_width;
+        unsigned_vector m_slice_width;
         // Cut point: if slice represents bit-vector x, then x has been sliced into x[|x|-1:cut+1] and x[cut:0].
         // The cut point is relative to the parent slice (rather than a root variable, which might not be unique)
         // (UINT_MAX for leaf slices)
-        unsigned_vector     m_slice_cut;
+        unsigned_vector m_slice_cut;
         // The sub-slices are at indices sub and sub+1 (null_slice if no subdivision)
         slice_vector    m_slice_sub;
         slice_vector    m_find;         // representative of equivalence class
         slice_vector    m_size;         // number of elements in equivalence class
         slice_vector    m_next;         // next element of the equivalence class
 
+        unsigned_vector m_slice2var;    // slice -> pvar, or null_var if slice is not equivalent to a variable
         slice_vector    m_var2slice;    // pvar -> slice
 
         slice alloc_slice();
 
         slice var2slice(pvar v) const { return find(m_var2slice[v]); }
+        pvar slice2var(slice s) const { return m_slice2var[find(s)]; }
         unsigned width(slice s) const { return m_slice_width[s]; }
         bool has_sub(slice s) const { return m_slice_sub[s] != null_slice; }