From 24b35fb9256f2bf799cadae819334d8d52a3e686 Mon Sep 17 00:00:00 2001
From: TheRealNebus <miguel.a.t.neves@gmail.com>
Date: Thu, 26 Apr 2018 22:42:55 +0100
Subject: [PATCH] WMax conflict budget bug fix

---
 src/opt/wmax.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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");