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;