From b154667092535605cc6d1334fa782e004f1f9033 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 24 Jan 2026 08:16:08 -1000 Subject: [PATCH] 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) --- src/math/lp/dioph_eq.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 57db6e79f..acc76bb11 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -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(); } };