diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index a76d4cb80..b462e2ac1 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -198,7 +198,9 @@ namespace polysat {
         }
     }
 
-    void slicing::explain(slice x, slice y, dep_vector& out_deps) {
+    void slicing::explain_base(slice x, slice y, dep_vector& out_deps) {
+        SASSERT(!has_sub(x));
+        SASSERT(!has_sub(y));
         //                   /-> ...
         // x -> x1 -> x2 -> lca <- y1 <- y
         //  r0   r1    r2         r4   r3
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 5aa074a8c..3c426d998 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -133,7 +133,8 @@ namespace polysat {
         // Returns true if merge succeeded without conflict.
         [[nodiscard]] bool merge_base(slice s1, slice s2, dep_t dep);
 
-        void explain(slice x, slice y, dep_vector& out_deps);
+        // Extract reason for equality of base slices
+        void explain_base(slice x, slice y, dep_vector& out_deps);
 
         // Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k
         //