diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 3df2fbf741..4ee29a8efc 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -74,7 +74,7 @@ private: m_val2fixed_row.insert(val(v1), r1); return; } - if (!only_one_nfixed(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) { + if (!only_one_nfixed(r2, v2) || ival(v1) != ival(v2) || is_int(v1) != is_int(v2)) { m_val2fixed_row.insert(val(v1), r1); return; } @@ -331,6 +331,12 @@ public: if (column_is_fixed(v_j)) { return; } + // the columns registered in the fixed tables have a zero infinitesimal part, + // so v_j cannot be equal to any of them when its delta part is not zero + if (!ival(v_j).y.is_zero()) { + try_add_equation_with_internal_fixed_tables(row_index); + return; + } unsigned j = null_lpvar; if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) { try_add_equation_with_internal_fixed_tables(row_index);