SA walk desyncs on object ==: the refEquals helper no longer matches the extractor's RefEqualityEmitter #100

Status: confirmed by reading the code; the effect on verdicts has not been measured in a run yet.

What happens

SWAT rewrites every IF_ACMPEQ/IF_ACMPNE into a call to UtilInstrumented.refEquals, whose branches are recorded in the trace. The static pre-analysis graph models those branches inline at the comparison (cfg-extraction RefEqualityEmitter), so the two must report the same branches in the same order.

Since 0152059 ("Reproduce Java reference identity in the IF_ACMP rewrite"), refEquals branches on instanceof String, string pooling (RefIdentity.isCanonicalString, isPooledOnly), RefIdentity.same, isCanonicalBox and the box cache range: 2 to about 9 branch events, depending on the runtime types. RefEqualityEmitter (cfg-extraction, unchanged since 2026-09-27) still models the old helper with two branches (shouldUseValueEquality, then a != b).

Effect (expected)

• The helper's branches carry no branch key, so the walk is only checked again at the next keyed branch. Comparisons of distinct objects (3 or more events), including enum comparisons, should therefore make the walk desync: sa_desync, and a SAFE verdict becomes UNKNOWN.
• If the next graph node has no key, or only an open ordinal (|*), the shifted pairing may go unnoticed: a residual false SAFE risk.
• sa-soundness/ref-eq* in targets/sv-comp/swat-benchmarks should show it; its result in RESULTS.md predates 0152059.

Fix

Either mask the helper's branches in the walk (as for choice branches and callbacks: the executor flags them and dfs holds the walk's place), or update RefEqualityEmitter to the new helper. Masking keeps the two repositories independent of the helper's implementation.

• References: symbolic-executor/.../common/UtilInstrumented.java:36, cfg-extraction src/main/java/de/uzl/its/cfg/extractor/RefEqualityEmitter.java.