[WIP] Leaks

[Copilot]

Starting investigation of memory leaks in Z3 solver. The issue shows two main leak sources:

• Analyze the memory leak stack traces provided in the issue
• Examine heap allocation in src/util/heap.h and vector expansion in src/util/vector.h
• Investigate var_register and lar_solver allocation patterns
• Identify where cleanup should happen but doesn't
• Explore memory management in src/util/memory_manager.cpp
• Look at solver lifecycle and finalization code
• Implement minimal fix for proper cleanup
• Test fix to ensure leaks are resolved
• Verify no new issues are introduced

Analysis Complete

Based on the stack traces, the leaks appear to be:

1. Heap allocation leak: heap<lp::lpvar_lt>::set_bounds -> heap constructor -> vector resize -> vector expand_vector -> memory::reallocate

2. Var register leak: var_register::add_var -> unordered_map allocation in lar_solver

Root Cause Identified

The memory leaks occur because:

1. During theory_lra::imp::init(), the solver calls get_one() and get_zero() which create variables via add_const()
2. These calls result in lar_solver::add_var() being called, which calls m_imp->m_var_register.add_var()
3. The var_register::add_var() method adds entries to m_external_to_local (unordered_map) and m_local_to_external (vector)
4. Although the var_register class has a clear() method, it's not being called during cleanup
5. The lar_solver destructor only deletes terms but doesn't clean up the var_register data structures

Fix Applied

Added a call to m_imp->m_var_register.clear() in the lar_solver::~lar_solver() destructor to properly clean up the var_register's data structures including the unordered_map and vector.

The fix is minimal and surgical - it only adds one line to ensure proper cleanup of the var_register when the lar_solver is destroyed.

Fixes #7690.

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

[NikolajBjorner]

You need to build z3 with Leak detection on using the address sanitizer, such as -fsanitize=address and other flags that are required for leak detection. Figure out what are the right flags before building z3.

[Copilot]

You need to build z3 with Leak detection on using the address sanitizer, such as -fsanitize=address and other flags that are required for leak detection. Figure out what are the right flags before bui...

I've built Z3 with address sanitizer using -fsanitize=address -fno-omit-frame-pointer -fsanitize-address-use-after-scope flags and ASAN_OPTIONS=detect_leaks=1.

Testing revealed that my initial fix was partial - it reduced leaks from 19520 bytes in 151 allocations to 19360 bytes in 141 allocations. The main issue was that the lar_solver destructor was missing dealloc(m_imp) to properly deallocate the implementation pointer.

With the complete fix (commit 43c35e4), Z3 now runs cleanly with no memory leaks detected by AddressSanitizer.