fix #7245

Z3Prover · Jun 15, 2024 · 01e47bf · 01e47bf
1 parent a6b5027
commit 01e47bf
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 11 deletions.
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
@@ -259,8 +259,9 @@ namespace opt {
         if (!m_models[i]) 
             m_models.set(i, m_last_model.get());
 
-        if (val > m_objective_values[i])
-            m_objective_values[i] = val;    
+        if (val > m_objective_values[i]) {
+            m_objective_values[i] = val;
+        }
 
         if (!m_last_model)
             return true;
@@ -284,14 +285,7 @@ namespace opt {
         // 
         auto check_bound = [&]() {
             SASSERT(has_shared);
-            bool ok = bound_value(i, val);
-            if (l_true != m_context.check(0, nullptr))  
-                return false;
-            m_context.get_model(m_last_model);
-            if (!m_last_model)
-                return false;
-            update_objective();
-            return ok;
+            return bound_value(i, val) && l_true == m_context.check(0, nullptr);
         };
 
         if (!val.is_finite()) {

diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
@@ -258,7 +258,7 @@ namespace smt {
         expr_ref_vector get_trail(unsigned max_level);
 
         /**
-           \brief (For debubbing purposes) Prints the state of the kernel
+           \brief (For debugging purposes) Prints the state of the kernel
         */
         std::ostream& display(std::ostream & out) const;