Fix push/pop scopes leaking learned clauses into subsequent proofs

[Copilot]

After push()/check-sat()/pop(), learned clauses involving only outer-scope variables survive gc_vars() and persist in the clause database, polluting watch lists and biasing VSIDS activity scores for subsequent proofs outside the scope.

Approach

Track the user scope level at clause creation using a new 2-bit m_scope_lim field in the clause struct (uses 2 previously unused bits in the existing packed bitfield). During user_pop(), after gc_vars() removes clauses containing pop'd variables, learned clauses with scope_lim > new_scope_level are also removed.

The field saturates at 3, so the cleanup is precise for up to 3 levels of nested push/pop; popping to scope level ≥3 cannot distinguish level-N from level-N+1 clauses, but the common cases (1–2 nesting levels) are handled exactly.

The cleanup is controlled by the new sat.gc.learned_pop parameter (default true), which can be set to false to disable the feature for testing or profiling.

Changes

• sat_clause.h: Add m_scope_lim:2 bitfield and scope_lim()/set_scope_lim() accessors to clause.
• sat_clause.cpp: Initialize m_scope_lim = 0 in the constructor; copy it in copy_clause() so memory defragmentation preserves scope information.
• sat_solver.cpp (mk_nary_clause): Stamp each learned clause with the current user scope depth on creation.
• sat_solver.cpp (user_pop): After gc_vars(), sweep m_learned and detach/delete any clause whose scope_lim exceeds the new scope level, gated on m_config.m_gc_learned_pop.
• sat_params.pyg: Add gc.learned_pop (bool, default true) parameter.
• sat_config.h / sat_config.cpp: Add m_gc_learned_pop field and read it from params.
• src/test/sat_gc.cpp: New benchmark (tst_sat_gc) that uses a near-phase-transition 3-SAT formula (200 variables, ratio 4.5) with 3 push/pop cycles to demonstrate that gc.learned_pop=true removes ~6000 stale learned clauses that would otherwise accumulate. Runs in ~0.1 s.

[NikolajBjorner]

@copilot create a benchmark where this makes a difference. Add a parameter to enable-disable this feature to allow testing.

[Copilot]

@copilot create a benchmark where this makes a difference. Add a parameter to enable-disable this feature to allow testing.

Added in commit a636fb3:

Parameter: sat.gc.learned_pop (bool, default true) — gates the learned clause cleanup in user_pop. Pass false to disable and observe the pollution effect.

Benchmark (src/test/sat_gc.cpp, tst_sat_gc): sets up a near-phase-transition 3-SAT formula on 200 outer-scope variables (ratio 4.5), runs 3 push/pop cycles, and compares the learned clause count before the final check-sat. With the default gc.learned_pop=true the clause database is clean (0 extra clauses); with gc.learned_pop=false over 6000 stale clauses accumulate. The test runs in ~0.1 s.

The mechanism: conflicts during the inner-scope check that are derived entirely from outer-scope clauses (which carry no scope-guard literal) produce learned lemmas that survive gc_vars. The benchmark triggers this by using a formula dense enough that outer-scope conflicts arise naturally. The VERIFY(lrn_with <= lrn_without) assertion documents the invariant.

[NikolajBjorner]

the "fix" while plausible improvement for something has nothing to do with the original bug report.
The original bug report creates benchmarks that don't use the sat core (unless the user specified "sat.smt=true" which I didn't see)