mirror of
https://github.com/Z3Prover/z3
synced 2026-06-10 10:57:15 +00:00
a5495b78fa
MSVC ASan reports showed a container-overflow in LP tableau pivoting, reproducible from both examples and solver tests (issue #9781). The failure came from reading a `column_cell` through a reference after pivoting removed that entry from the backing column. - **Root cause** - `pivot_column_tableau` and the analogous Diophantine elimination loop both held `auto& c = column.back()` across a call (`pivot_row_to_row_given_cell`) that immediately removes that very cell from the column via `remove_element`. - After the mutation, the subsequent read `c.var()` used for bookkeeping observed invalid memory. - **Change** - Record the affected row in the bookkeeping set (`m_touched_rows` / `m_changed_rows`) by reading `c.var()` **before** the pivot call, while the back cell is still valid. - Make `static_matrix::pivot_row_to_row_given_cell` return `void` instead of `bool`. Its result (`!rowii.empty()`) was always `true`: both callers keep the matrix at full row rank (the tableau basis columns form an identity submatrix; the Diophantine `m_l_matrix` stays invertible), so an elementary row operation can never empty a row. The dead `if (!...) return false;` early-exit in `pivot_column_tableau` is removed and replaced with a `SASSERT(!rowii.empty())` documenting the invariant. - **Affected code paths** - `src/math/lp/static_matrix.h`, `src/math/lp/static_matrix.cpp`, `src/math/lp/static_matrix_def.h` - `src/math/lp/lp_core_solver_base_def.h` - `src/math/lp/dioph_eq.cpp` - **Behavioral impact** - No algorithmic change to pivoting. - Removes the stale-reference hazard in the loops that repeatedly eliminate entries from a column. ```c++ while (column.size() > 1) { auto& c = column.back(); SASSERT(c.var() != piv_row_index); if (m_touched_rows != nullptr) m_touched_rows->insert(c.var()); m_A.pivot_row_to_row_given_cell(piv_row_index, c, j); } ``` - **Verification** - Reproduced the exact issue #9781 failure on a local ASan build (`container-overflow` in `pivot_column_tableau`) using the pre-fix code, and confirmed it is gone with this change. - The 4 reported tests pass clean under ASan: `c_example`, `cpp_example`, `test-z3 get_implied_equalities`, `test-z3 quant_solve`. - Full `test-z3 /a` suite: 89 passed, 0 failed, 0 ASan errors. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||