diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 436eb7130..581c75f5b 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -342,6 +342,8 @@ namespace polysat {
         pdd a = y;
         if (!is_Y_l_Ax(x, y_l_ax, a, y))
             return false;
+        if (a.is_one())
+            return false;
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;