From b74e35f4fba5bca70d0b6443a40250314f36fe25 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 28 May 2026 09:06:05 -0700
Subject: [PATCH] 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>
---
 src/math/polynomial/algebraic_numbers.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index ab70fc318..07b49e5ce 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -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);