Merge branch 'master' into unit_prop_on_monomials

Z3Prover · Sep 27, 2023 · 4b85a10 · 4b85a10
2 parents 94eb101 + 9c63ea3
commit 4b85a10
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
@@ -145,6 +145,7 @@ class lp_bound_propagator {
         return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero();
     }
 
+
     void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* ()> explain_bound) {
         j = lp().column_to_reported_index(j);
 
@@ -159,6 +160,7 @@ class lp_bound_propagator {
             if (m_improved_lower_bounds.find(j, k)) {
                 auto& found_bound = m_ibounds[k];
                 if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
+
                     found_bound.m_bound = v;
                     found_bound.m_strict = strict;
                     found_bound.set_explain(explain_bound);
@@ -174,6 +176,7 @@ class lp_bound_propagator {
             if (m_improved_upper_bounds.find(j, k)) {
                 auto& found_bound = m_ibounds[k];
                 if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
+
                     found_bound.m_bound = v;
                     found_bound.m_strict = strict;
                     found_bound.set_explain(explain_bound);