mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 23:27:53 +00:00
Code Activity

Merge pull request #8218 from Z3Prover/copilot/fix-segmentation-fault-ufnira

Browse source
This commit is contained in:
Lev Nachmanson 2026-01-17 05:18:38 -10:00 • committed by GitHub
commit d60373c5d5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1094,11 +1094,11 @@ namespace lp {
recalculate_entry(ei); recalculate_entry(ei);
if (m_e_matrix.m_columns.back().size() == 0) { if (!m_e_matrix.m_columns.empty() && m_e_matrix.m_columns.back().size() == 0) {
m_e_matrix.m_columns.pop_back(); m_e_matrix.m_columns.pop_back();
m_var_register.shrink(m_e_matrix.column_count()); m_var_register.shrink(m_e_matrix.column_count());
} }
if (m_l_matrix.m_columns.back().size() == 0) if (!m_l_matrix.m_columns.empty() && m_l_matrix.m_columns.back().size() == 0)
m_l_matrix.m_columns.pop_back(); m_l_matrix.m_columns.pop_back();
} }
remove_irrelevant_fresh_defs(); remove_irrelevant_fresh_defs();