3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00

Fix memory leak in mpz pointer tagging implementation

The memory leak was caused by mpz_manager::set() methods that would
directly overwrite the m_value field when setting small values, without
first deallocating any existing large value. This resulted in leaked
memory when transitioning from large to small integers.

Fixed by adding deallocate() calls before setting small values in:
- set(mpz& target, mpz const& source)
- set(mpz& a, int val)
- set(mpz& a, uint64_t val)
- set_i64(mpz& c, int64_t v)

The deallocate() method safely handles the case when the value is already
small (it's a no-op in that case), so this fix is safe for all scenarios.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-08 22:44:28 +00:00
parent 58df141825
commit 64d5544a32

View file

@ -299,6 +299,7 @@ class mpz_manager {
void set_i64(mpz & c, int64_t v) {
if (v >= INT_MIN && v <= INT_MAX) {
deallocate(c); // Free any existing large value before setting small
c.set(static_cast<int>(v));
}
else {
@ -589,6 +590,7 @@ public:
void set(mpz & target, mpz const & source) {
if (is_small(source)) {
deallocate(target); // Free any existing large value before setting small
target.set(source.value());
}
else {
@ -597,6 +599,7 @@ public:
}
void set(mpz & a, int val) {
deallocate(a); // Free any existing large value before setting small
a.set(val);
}
@ -615,6 +618,7 @@ public:
void set(mpz & a, uint64_t val) {
if (val < INT_MAX) {
deallocate(a); // Free any existing large value before setting small
a.set(static_cast<int>(val));
}
else {