3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 14:17:47 +00:00

Fix mpz_manager leak in algebraic root comparison (#9654)

A `root-obj`-driven unsat case was exiting with a leaked `mpz_manager`
allocation even though solver output was correct. The leak came from
temporary rational bounds created during algebraic-number comparison and
not released before shutdown.

- **Root cause**
- `algebraic_numbers::compare_core()` materialized interval bounds as
raw `mpq` temporaries.
- Those temporaries could allocate backing `mpz` storage, but their
lifetime was not tied to the manager, so the allocator retained leaked
cells at process exit.

- **Change**
- Replace the raw `mpq` temporaries with `scoped_mpq` in
`/src/math/polynomial/algebraic_numbers.cpp`.
- This keeps the comparison logic unchanged while making temporary bound
conversion use RAII-managed cleanup.

- **Effect**
- `root-obj` comparisons no longer leave `mpz_manager` allocations
behind.
- Solver behavior is unchanged; the fix is limited to temporary numeral
lifetime management.

```c++
- mpq l_a, u_a, l_b, u_b;
+ scoped_mpq l_a(qm()), u_a(qm()), l_b(qm()), u_b(qm());
```

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-05-28 09:06:05 -07:00 committed by GitHub
parent 0b56db7f07
commit b74e35f4fb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -2032,7 +2032,7 @@ namespace algebraic_numbers {
// Check whether a can be separated from b's interval and vice versa
// this recognizes the case where the intervals overlap,
// but the anums do not lie in the intersection of the intervals.
mpq l_a, u_a, l_b, u_b;
scoped_mpq l_a(qm()), u_a(qm()), l_b(qm()), u_b(qm());
to_mpq(qm(), la, l_a);
to_mpq(qm(), ua, u_a);
to_mpq(qm(), lb, l_b);