Member predicate MakeWithSplitting::SplitImplementations::ConditionalCompletionSplitting::ConditionalCompletionSplitImpl::hasExit
Holds if this split is left when control passes from pred
to succ
with
completion c
.
Invariant: hasExit(pred, succ, c) implies succ(pred, succ, c)
.
predicate hasExit(AstNode pred, AstNode succ, Completion c)