fix #4233

src/opt/wmax.cpp

@@ -54,7 +54,7 @@ namespace opt {
         lbool operator()() override {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
-            obj_map<expr, rational> soft;            
+            obj_map<expr, rational> soft;
             reset();
             lbool is_sat = find_mutexes(soft);
             if (is_sat != l_true) {
@@ -64,19 +64,18 @@ namespace opt {
             expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
 
-            obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
-            for (; it != end; ++it) {
-                assert_weighted(wth(), it->m_key, it->m_value);
-                if (!is_true(it->m_key)) {
-                    m_upper += it->m_value;
+            for (auto const& kv : soft) {
+                assert_weighted(wth(), kv.m_key, kv.m_value);
+                if (!is_true(kv.m_key)) {
+                    m_upper += kv.m_value;
                 }
             }
             wth().init_min_cost(m_upper - m_lower);
             trace_bounds("wmax");
-            
-            TRACE("opt", 
-                  s().display(tout)<< "\n";
-                  tout << "lower: " << m_lower << " upper: " << m_upper << "\n";);
+
+            TRACE("opt",
+                s().display(tout) << "\n";
+            tout << "lower: " << m_lower << " upper: " << m_upper << "\n";);
             while (m.inc() && m_lower < m_upper) {
                 is_sat = s().check_sat(0, nullptr);
                 if (!m.inc()) {
@@ -104,8 +103,9 @@ namespace opt {
                 SASSERT(m_lower <= m_upper);
             }
 
-            update_assignment();
-
+            if (m_model) 
+                update_assignment();
+
             if (m.inc() && is_sat == l_undef && m_lower == m_upper) {
                 is_sat = l_true;
             }