mirror of
https://github.com/Z3Prover/z3
synced 2026-01-26 20:08:42 +00:00
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)
This commit is contained in:
parent
1cf9ba152b
commit
b154667092
1 changed files with 4 additions and 1 deletions
|
|
@ -654,13 +654,16 @@ namespace lp {
|
|||
struct undo_fixed_column : public trail {
|
||||
imp& m_imp;
|
||||
unsigned m_j; // the column that has been added
|
||||
const mpq m_fixed_val;
|
||||
mpq m_fixed_val; // not const: needs to be reset in undo() to free heap memory
|
||||
undo_fixed_column(imp& s, unsigned j) : m_imp(s), m_j(j), m_fixed_val(s.lra.get_lower_bound(j).x) {
|
||||
SASSERT(s.lra.column_is_fixed(j));
|
||||
}
|
||||
|
||||
void undo() override {
|
||||
m_imp.add_changed_column(m_j);
|
||||
// Free heap-allocated memory in m_fixed_val since this struct is region-allocated
|
||||
// and its destructor won't be called
|
||||
m_fixed_val.reset();
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue