From 1218520a6cb7d606f649b9c7319a59dcf962ef8c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Apr 2026 18:34:43 +0000 Subject: [PATCH] Improve comments in push/pop scope cleanup code Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c23a0600-90dd-45a1-b64f-c286d041f373 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/sat/sat_clause.h | 2 +- src/sat/sat_solver.cpp | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index f986e7e41..56bd35db6 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -53,7 +53,7 @@ namespace sat { unsigned m_inact_rounds:8; unsigned m_glue:8; unsigned m_psm:8; // transient field used during gc - unsigned m_scope_lim:2; // user scope level when clause was learned, saturated at 3 + unsigned m_scope_lim:2; // user scope level when clause was learned (0-3, saturated: levels >=4 map to 3) literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 33f6fd80c..dd0e67ae7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3724,12 +3724,15 @@ namespace sat { gc_vars(max_var); - // remove learned clauses that were added during the popped user scopes - // scope_lim is saturated at 3, so clauses at scope > old_sz can be identified when old_sz < 3 + // remove learned clauses that were added during the popped user scopes. + // scope_lim is saturated at 3, so when old_sz < 3 we can precisely identify + // and remove clauses learned at scope levels above old_sz. if (old_sz < 3) { unsigned j = 0; for (clause* c : m_learned) { if (c->scope_lim() > old_sz) { + // pop_to_base_level() ensures no clause is on the reinit stack at base level, + // so it is safe to detach and delete the clause. SASSERT(!c->on_reinit_stack()); detach_clause(*c); del_clause(*c);