Skip to main content

BRANCH_SENSITIVE_BACKEDGES

Constant BRANCH_SENSITIVE_BACKEDGES 

Source
const BRANCH_SENSITIVE_BACKEDGES: usize = DEFAULT_LOOP_CARRIED_BACKEDGES; // 3usize
Expand description

Backedge budget used when an internally branched SCC has loop-carried assignments into a checked sink.

This calibrates to allow_repeat = 2, which is enough to cover the shallow branch-sensitive SCC fixtures without pushing the enumerator into a large repeat where path limits may hide lower-depth witnesses.