The cfopt itself can handle unreachable code,
but it transforms it in a way that makes the verifier unhappy.