diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index c3f38d5ba..9e3c8d44f 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1591,7 +1591,7 @@ namespace polysat {
         if (y == null_var) {
             // choose the top variable
             y = q.var();
-            if (q.hi().is_var() && q.hi().var() == y)
+            if (!q.hi().is_val() && q.hi().var() == y)
                 return false;
             if (!eval_round(M, q.hi(), a))
                 return false;