pub fn congested_approach(width: u32, jam: u64) -> String
A queue served only every other cycle while one vehicle arrives each cycle: net inflow is positive, so the queue climbs to jam. BMC finds the cycle it overflows.
jam