weird latent bug in wmax: init() succeeds and it returns undef

Z3Prover · Apr 25, 2023 · d8156ae · d8156ae
1 parent fdd5c92
commit d8156ae
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
@@ -213,7 +213,8 @@ namespace opt {
             try {
                 is_sat = (*m_msolver)();
             }
-            catch (z3_exception&) {
+            catch (z3_exception& ex) {
+                IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n");
                 is_sat = l_undef;
             }
             if (is_sat != l_false) {

diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
@@ -53,7 +53,7 @@ namespace opt {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
             reset();
-            if (init())
+            if (!init())
                 return l_undef;
 
             lbool is_sat = l_true;