Predicate bbSuccessorEntryReachesLoopInvariant

Loop invariant for bbSuccessorEntryReaches:

• succ is a successor of pred.
• predSkipsFirstLoopAlwaysTrueUponEntry: whether the path from pred (via succ) skips the first loop where the condition is provably true upon entry.
• succSkipsFirstLoopAlwaysTrueUponEntry: whether the path from succ skips the first loop where the condition is provably true upon entry.
• If pred contains the entry point of a loop where the condition is provably true upon entry, then succ is not allowed to skip that loop (succSkipsFirstLoopAlwaysTrueUponEntry = false).