From bb735588488f90675cca78c286b35a50bca52af7 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 30 Jun 2026 12:35:06 +0200 Subject: [PATCH] Fixed memory corruption --- src/smt/nseq_context_solver.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index ba4fb091a1..f7370cd511 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -57,7 +57,6 @@ namespace smt { svector m_frame_bounds; // m_deps.size() at each push() svector m_deps; // id -> dep - // Scratch dep_manager for joining core deps; reset before each check(). seq::dep_manager m_core_dep_mgr; seq::dep_tracker m_last_core = nullptr; @@ -75,7 +74,8 @@ namespace smt { } lbool check() override { - m_core_dep_mgr.reset(); + // do NOT reset m_core_dep_mgr here. Core trees + // returned by core() outlive this call. It is reset only in reset(). m_last_core = m_core_dep_mgr.mk_empty(); lbool r; if (m_assump_lits.empty()) {