Function chosen_successor 

fn chosen_successor(
    path: &Path,
    block: BasicBlock,
    occurrence: usize,
) -> Option<BasicBlock>

Return the next MIR block after block in a finite verification path.