From b3f977d06c30cc9f0eb84838be8e17dd4bbbf7c5 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Mon, 30 Mar 2026 04:58:45 -1000
Subject: [PATCH] Fix nlsat clear crash (#9150)

* fix nlsat clear() and scoped_numeral_vector copy ctor crashes

Reset polynomial cache and assignments in nlsat::solver::imp::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>