From d8156aeff31fb224531b026daacfafe2222f00e7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Apr 2023 21:14:42 -0700
Subject: [PATCH] weird latent bug in wmax: init() succeeds and it returns
 undef

---
 src/opt/maxsmt.cpp | 3 ++-
 src/opt/wmax.cpp   | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 37f888120..e684c64d6 100644
--- 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
index 1fb6c05dd..9a7d1a3ca 100644
--- 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;