Member predicate ControlFlow::Internal::SplitInternal::hasSuccessor

Holds if this split is maintained when control passes from pred to succ with completion c.

Invariant: hasSuccessor(pred, succ, c) implies succ = Successor::succ(pred, c)

predicate hasSuccessor(ControlFlowElement pred, ControlFlowElement succ, Completion c)