Fix nlsat clear crash (#9150)

Browse source

* 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>

...

This commit is contained in:

Lev Nachmanson 2026-03-30 04:58:45 -10:00 • committed by GitHub

parent 1f506ee242

commit b3f977d06c

No known key found for this signature in database

GPG key ID: B5690EEEBB952194

Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL

Download patch file Download diff file Expand all files Collapse all files

Diff content is not available