From 75baedb314791c9e516e6166176b5becba9fc4ef Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Mar 2026 11:09:19 -1000 Subject: [PATCH] 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> --- src/nlsat/nlsat_solver.cpp | 4 ++++ src/util/scoped_numeral_vector.h | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 6a656b46d..b68e642bc 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -347,6 +347,10 @@ namespace nlsat { undo_until_size(0); del_clauses(); del_unref_atoms(); + m_cache.reset(); + m_assignment.reset(); + m_lo.reset(); + m_hi.reset(); } void checkpoint() { diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index b5cfb69cb..44e625550 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -28,7 +28,7 @@ public: _scoped_numeral_vector(const _scoped_numeral_vector & other) : m_manager(other.m_manager) { for (unsigned i = 0, e = other.size(); i != e; ++i) { - push_back((*this)[i]); + push_back(other[i]); } }