diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 4999eabc7..9fe444301 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1744,9 +1744,18 @@ namespace polysat {
                 return l_true;  // done
 
             SASSERT(result == l_undef);
-            // TODO: continue with intervals at current level
+
+            if (progress >= mod_value) {
+                // covered the whole domain => conflict
+                return l_false;
+            }
+
+            if (progress >= to_cover_len) {
+                // we covered the hole left at larger bit-width
+                return l_undef;
+            }
         }
-        NOT_IMPLEMENTED_YET();
+        UNREACHABLE();
         return l_undef;
     }