3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-16 10:10:02 +00:00
z3/src
Lev Nachmanson 6bce4c2b81 Fix memory leak in undo_fixed_column for big numbers
The undo_fixed_column struct is region-allocated via trail_stack, so its
destructor is never called. When m_fixed_val contains a big number (one
that doesn't fit in a small int), the heap-allocated memory for the mpq
numerator/denominator was never freed.

Fix by calling m_fixed_val.reset() in undo() to explicitly free the
heap memory before the region deallocates the struct.

Verified with macOS leaks tool:
- Before: 126 leaks (6048 bytes) on convert-jpg2gif-query-1584.smt2
- After: 0 leaks on normal completion, 10 leaks on timeout (unfinished trail)
2026-02-18 20:57:54 -08:00
..
ackermannization Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
api preserve the initial state of the solver with push/pop for multiple objectives (#8264) 2026-02-18 20:57:53 -08:00
ast Refactor arith_rewriter::find_nl_factor() to use std::optional (#8313) 2026-02-18 20:57:53 -08:00
cmd_context Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-02-18 20:57:52 -08:00
math Fix memory leak in undo_fixed_column for big numbers 2026-02-18 20:57:54 -08:00
model Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
muz Refactor sym_mux::find_idx to use std::optional (#8293) 2026-02-18 20:57:53 -08:00
nlsat Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
opt preserve the initial state of the solver with push/pop for multiple objectives (#8264) 2026-02-18 20:57:53 -08:00
params Add SLS tactic as a separate worker thread (#8263) 2026-02-18 20:57:50 -08:00
parsers Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
qe Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-02-18 20:57:52 -08:00
sat Refactor mk_and and mk_app to use std::span API (#8285) 2026-02-18 20:57:52 -08:00
shell Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt Refactor dyn_ack propagate_eh to use structured bindings (#8317) 2026-02-18 20:57:54 -08:00
solver Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
tactic Refactor mk_and and mk_app to use std::span API (#8285) 2026-02-18 20:57:52 -08:00
test preserve the initial state of the solver with push/pop for multiple objectives (#8264) 2026-02-18 20:57:53 -08:00
util deal with build warnings 2026-02-18 20:57:53 -08:00
CMakeLists.txt BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 2026-02-18 20:57:00 -08:00