diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 52b87e536..513c68d6e 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -84,6 +84,9 @@ namespace opt {
                 if (m.canceled()) {
                     is_sat = l_undef;
                 }
+                if (is_sat == l_undef) {
+                    break;
+                }
                 if (is_sat == l_false) {
                     TRACE("opt", tout << "Unsat\n";);
                     break;
@@ -97,9 +100,6 @@ namespace opt {
                     //DEBUG_CODE(verify_cores(cores););
                     s().assert_expr(fml);
                 }
-                else {
-                    //DEBUG_CODE(verify_cores(cores););
-                }
                 update_cores(wth(), cores);
                 wth().init_min_cost(m_upper - m_lower);
                 trace_bounds("wmax");