mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

Fix ASAN memory leak by removing unused m_fixed_val in undo_fixed_column (#10199)

Browse source 
Remove unused m_fixed_val member variable from undo_fixed_column.

undo_fixed_column is allocated in a region/trail allocator where C++
destructors are not invoked when objects are popped/reclaimed. Storing
an mpq instance (which can allocate heap memory for multi-precision
numbers) inside a region-allocated object causes a memory leak that is
flagged by ASAN.

m_fixed_val was never used in undo() or elsewhere in the struct.
Removing it completely eliminates the ASAN finding, avoids unnecessary
mpq copies, and is entirely safe.
This commit is contained in:
l46kok 2026-07-23 09:03:08 -07:00 • committed by GitHub
parent aba41d026f
commit 8a9beaf882
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/dioph_eq.cpp
View file

@ -649,16 +649,12 @@ namespace lp {
struct undo_fixed_column : public trail {
imp& m_imp;
unsigned m_j; // the column that has been added
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) {
undo_fixed_column(imp& s, unsigned j) : m_imp(s), m_j(j) {
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();
}
};