From 4936ace7cdf99e8d5bdc5e164647117451cf8b1c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 5 Jun 2020 13:50:46 -0700 Subject: [PATCH] more guards on cheap_eqs Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 3 +++ src/math/lp/lp_bound_propagator.h | 8 ++++++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f479b4d33..5f757747e 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -158,9 +158,12 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { } unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { + SASSERT(j < m_var_register.size()); if (!tv::is_term(j)) { unsigned ext_var_or_term = m_var_register.local_to_external(j); j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term; + } else { + UNREACHABLE(); } return j; } diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 80040a88b..a919537fb 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -214,8 +214,12 @@ public: display_row_of_vertex(v_j, tout); ); lp::explanation exp = get_explanation_from_path(v_i, path, v_j); - unsigned i_e = lp().adjust_column_index_to_term_index(get_column(m_vertices[v_i])); - unsigned j_e = lp().adjust_column_index_to_term_index(get_column(m_vertices[v_j])); + lpvar v_i_col = get_column(m_vertices[v_i]); + lpvar v_j_col = get_column(m_vertices[v_j]); + if (lp().column_is_int(v_i_col) != lp().column_is_int(v_j_col)) + return; + unsigned i_e = lp().adjust_column_index_to_term_index(v_i_col); + unsigned j_e = lp().adjust_column_index_to_term_index(v_j_col); m_imp.add_eq(i_e, j_e, exp); }