Reworked from static-witness-only to execution-driven: ~99% of SCJUMP decisions are gated by a native computed value (op 0x60), so witness-synthesis alone can't cover them. Value-local tracking resolves load-then-compare guards to real globals; native terms honestly marked opaque. Verify: static 3/3 exact + 279/279 execution- driven consistent over 2000 seeds, 0 failures. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
16 KiB
16 KiB