mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

out of bounds fixes

Browse source
This commit is contained in:
Lev Nachmanson 2025-02-03 07:12:42 -10:00 • committed by Lev Nachmanson
parent 3b3d8cee03
commit 21f67ef942
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/dioph_eq.cpp
View file

@ -926,6 +926,7 @@ namespace lp {
}
find_changed_terms_and_more_changed_rows();
for (unsigned j : m_changed_terms) {
if (j >= m_l_matrix.column_count()) continue;
for (const auto & cs: m_l_matrix.column(j)) {
m_changed_rows.insert(cs.var());
}
@ -1328,6 +1329,7 @@ namespace lp {
lia_move ret = lia_move::undef;
for (unsigned j : m_changed_terms) {
cleanup.push_back(j);
if (j >= lra.column_count()) continue;
if (!lra.column_has_term(j) || lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) {
continue;