From aa0f5db5116cfd9624f93ef1f6249c8c4b1f93dd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 27 Apr 2020 15:43:59 -0700 Subject: [PATCH] fixes Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index bdaf32e88..c5396b2f9 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1774,8 +1774,13 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1)); if (use_lu()) fill_last_row_of_A_d(A_d(), term); - for (const auto & c : *term) - m_usage_in_terms[c.column()] = m_usage_in_terms[c.column()] + 1; + for (const auto & c : *term) { + unsigned j = c.column(); + while (m_usage_in_terms.size() <= j) { + m_usage_in_terms.push_back(0); + } + m_usage_in_terms[j] = m_usage_in_terms[j] + 1; + } }