From e760eabd2bfe76fd275806fc454d9b419339dc9b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Mar 2026 20:01:04 -1000 Subject: [PATCH] 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> --- src/nlsat/nlsat_solver.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index b68e642bc..6a656b46d 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -347,10 +347,6 @@ 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() {