diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index e08965e54..f8534937b 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1973,15 +1973,20 @@ namespace polysat {
         //      e.g.:   v^2 + w^2 == 0;   w := 1
         // - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v):
         //      e.g.:   v^2 + w^2 == 0;   w^2 == 1
+        uint_set to_explain;
         for (unsigned d : us.unsat_core()) {
             auto [x, lit] = deps[d];
-            s.m_slicing.explain_simple_overlap(v, x, [this, &core](sat::literal l) {
-                core.insert(s.lit2cnstr(l));
-            });
+            if (x != v)
+                to_explain.insert(x);
             signed_constraint c = s.lit2cnstr(lit);
             core.insert(c);
             core.insert_vars(c);
         }
+        for (pvar x : to_explain) {
+            s.m_slicing.explain_simple_overlap(v, x, [this, &core](sat::literal l) {
+                core.insert(s.lit2cnstr(l));
+            });
+        }
         SASSERT(!core.vars().contains(v));
         core.add_lemma("viable unsat core", core.build_lemma());
         IF_VERBOSE(10, verbose_stream() << "unsat core " << core << "\n";);