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>
- Remove .csproj overwrite in macOS x64 and ARM64 NuGet jobs that
replaced the versioned PackageReference with Version="*", causing
FileNotFoundException for Microsoft.Z3 assembly
- Add validate-build-script-tests job to run scripts/tests/test_*.py,
ensuring JNI arch flag tests from PR #8896 are exercised nightly
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Calling factor_sqf_pp recursively on Hensel-lifted factors corrupts
shared mutable state in the polynomial manager, m_m2pos, m_som_buffer,
m_cheap_som_buffer, m_tmp1, etc., causing assertion violations:
- polynomial.cpp:473 id < m_m2pos.size()
- upolynomial.cpp:2624 sign_a == -sign_b
Use factor_1_sqf_pp/factor_2_sqf_pp for small degrees, push directly
for larger degrees. These don't conflict with the outer call's buffers.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Fix memory leaks: use scoped_numeral instead of raw numeral for
evaluation points, ensuring cleanup on exceptions
- Precompute lc_inv before the Hensel lifting loop instead of
recomputing each iteration
- Use scoped_numeral_vector for eval_vals for consistency with codebase
- Move eval_values and candidate_primes to static constexpr class-level
- Document limitations: single-prime Hensel lifting, contiguous factor
splits only, pseudo-division lc-power caveat
- Condense Bezout derivation comment to 4-line summary
- Fix README to say Hensel lifting instead of GCD recovery
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the stub factor_n_sqf_pp (TODO: invoke Dejan's procedure) with a
working implementation using bivariate Hensel lifting:
- Evaluate away extra variables to reduce to bivariate
- Factor the univariate specialization
- Lift univariate factors to bivariate via linear Hensel lifting in Zp[x]
- Verify lifted factors multiply to original over Z[x,y]
- For >2 variables, check bivariate factors divide the original polynomial
Tests: (x0+x1)(x0+2x1)(x0+3x1) now correctly factors into 3 linear factors.
All 89 unit tests pass in both release and debug builds.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
