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.