diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 3b0f684e8..8f77cdf85 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -39,6 +39,9 @@ namespace opt {
             if (m_maxsat_engine == symbol("core_maxsat")) {
                 m_msolver = alloc(core_maxsat, m, s, m_soft_constraints);
             }
+            else if (m_maxsat_engine == symbol("weighted_maxsat")) {
+                m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights);
+            }
             else {
                 m_msolver = alloc(fu_malik, m, s, m_soft_constraints);
             }
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 6c4e99d7e..1d2aa22a6 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -253,6 +253,7 @@ namespace smt {
                 disj.push_back(m.mk_not(m_min_cost_atom));
             }
             if (is_optimal()) {
+                IF_VERBOSE(1, verbose_stream() << "(wmaxsat with lower bound: " << weight << "\n";);
                 m_min_cost = weight;
                 m_cost_save.reset();
                 m_cost_save.append(m_costs);