new command &scorr2 extended from &scorr

[zxxr1113]

Summary

This PR introduces &scorr2, a new signal correspondence command that is a complete, re-architected version of the incremental refinement engine from &scorr -i (previously merged in PR #529). Unlike the original &scorr -i which was retrofitted into the existing engine, &scorr2 has its own dedicated engine (Cec_ManLSCorrespondence2) designed from the ground up for the incremental workflow.

Key Features

Incremental refinement engine (cecCorr2.c)

• All incremental optimizations enabled by default (-iDI): incremental TFO-triggered re-proof, dynamic SRM construction, event-driven resimulation
• Persistent dynamic SRM (cecCorrDyn.c) that accumulates refinement across iterations
• Event-driven incremental resimulation (cecCorrIncrSim.c) for efficient candidate propagation
• Adaptive BMC solver policy (-Y): guarded CBS-first/TAS-rescue strategy to minimize solver time
• Clean module separation: each component in its own file

-K strict fixed-point oracle audit

• After the main loop converges, the -K flag triggers a Kissat-based certification pass that rebuilds the complete SRM and independently certifies the final signal correspondence
• Audits both inductive-step and base-phase obligations
• If certification fails, the reduction is rejected — this is a safety checker, not a repair pass
• Useful for debugging and validating correctness of the optimized incremental pipeline

Other options

• -D: toggle persistent dynamic SRM construction
• -I: toggle event-driven resimulation
• -s: skip resimulation without a real CEX
• -Y: adaptive CBS-first/TAS-rescue BMC policy

Files Changed

Area	Files	Description
&scorr2 engine	cecCorr2.c (2274 lines)	Main incremental correspondence engine
Incremental sim	cecCorrIncrSim.c (2202 lines)	Event-driven resimulation manager
Dynamic SRM	cecCorrDyn.c (1213 lines)	Persistent dynamic SRM construction
Incremental re-proof	cecCorrIncr.c (690 lines)	TFO-triggered incremental re-proof
Kissat oracle	cecCorrCert.c (155 lines)	Certification helper for -K
Interface	cecInt.h	Extended parameter and API definitions
Command	abc.c	&scorr2 command registration

Relationship to &scorr -i

&scorr -i (PR #529) introduced incremental refinement as an option. &scorr2 takes this further with a dedicated engine where the incremental workflow is the central design, enabling cleaner module separation, the -K oracle certification, and aggressive defaults that reflect the incremental approach's maturity.

Usage

&scorr2 [-FCGXPSZ num] [-pkrecqiDIsYKovh]

Typical: &scorr2 -K (incremental correlation with final Kissat oracle audit)