* fix nlsat clear() and scoped_numeral_vector copy ctor crashes
Reset polynomial cache and assignments in nlsat::solver:👿:clear()
to prevent use-after-free when the solver is destroyed. The missing
resets caused heap corruption when check_assignment's
compute_linear_explanation created cached polynomials and root atoms
that outlived the solver's other data structures during destruction.
Also fix _scoped_numeral_vector copy constructor to read from other
instead of uninitialized self.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* simplify scoped_numeral_vector copy constructor loop
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* revert clear() additions that cause heap corruption
The m_cache.reset(), m_assignment.reset(), m_lo.reset(), m_hi.reset()
calls added to clear() in commit 481eb0327 cause heap corruption when
clear() is called from the destructor. The cache reset frees polynomials
while the polynomial manager still holds references to them, corrupting
the heap. This manifests as 'corrupted double-linked list' crashes
during nlsat solver destruction in the nra check path.
The reset() method already has these calls for solver reuse. The
destructor path via clear() should not duplicate them, as implicit
member destruction handles cleanup in the correct order.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* fix heap corruption from root_function move/sort operations
root_function's move constructor and move assignment were doing deep
copies of algebraic numbers via anum_manager::set() instead of proper
moves. During std::vector reallocation (emplace) and std::sort, this
caused massive allocation churn that corrupted the heap.
Fixes:
1. Move constructor: use std::move(other.val) for proper swap semantics.
2. Move assignment: use val.swap(other.val) instead of deep copy.
3. Add friend swap() for ADL so std::sort uses efficient swaps.
4. Sort root_function partitions via index permutation + swap cycles
instead of std::sort directly on root_function objects.
5. Reserve rfunc vector before emplace in add_linear_approximations().
6. Reserve lhalf/uhalf vectors before collecting root functions.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Fix apply_permutation to take perm by const reference
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f81ba8ad-2875-4fcc-ba91-d502905756be
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
root_function's move constructor and move assignment were doing deep
copies of algebraic numbers via anum_manager::set() instead of proper
moves. During std::vector reallocation (emplace) and std::sort, this
caused massive allocation churn that corrupted the heap.
Fixes:
1. Move constructor: use std::move(other.val) for proper swap semantics.
2. Move assignment: use val.swap(other.val) instead of deep copy.
3. Add friend swap() for ADL so std::sort uses efficient swaps.
4. Sort root_function partitions via index permutation + swap cycles
instead of std::sort directly on root_function objects.
5. Reserve rfunc vector before emplace in add_linear_approximations().
6. Reserve lhalf/uhalf vectors before collecting root functions.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The m_cache.reset(), m_assignment.reset(), m_lo.reset(), m_hi.reset()
calls added to clear() in commit 481eb0327 cause heap corruption when
clear() is called from the destructor. The cache reset frees polynomials
while the polynomial manager still holds references to them, corrupting
the heap. This manifests as 'corrupted double-linked list' crashes
during nlsat solver destruction in the nra check path.
The reset() method already has these calls for solver reuse. The
destructor path via clear() should not duplicate them, as implicit
member destruction handles cleanup in the correct order.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Reset polynomial cache and assignments in nlsat::solver:👿:clear()
to prevent use-after-free when the solver is destroyed. The missing
resets caused heap corruption when check_assignment's
compute_linear_explanation created cached polynomials and root atoms
that outlived the solver's other data structures during destruction.
Also fix _scoped_numeral_vector copy constructor to read from other
instead of uninitialized self.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
