Description
When a join is performed at a loop head, the resulting flow condition will naively grow redundant clauses with each iteration over the loop.
Assuming we enter a loop with FC1 and then add FC2 during analysis of the body, we end with FC1 and FC2. Currently, the join will produce FC1 or (FC1 and FC2). This is inefficient, so we should start by fixing the FC join operation to avoid situations like this and eagerly simplify to FC1.
There may be situations involving gotos that could look quite different, namely the loop body would end with D and the join therefore is C or D with no commonality. Moreover, another time through the loop will result in first D or (C or D) (after the join from the goto, assuming no further conditions are accumulated in the loop body) and then C or (D or (C or D)) when we join before the loop head. So, that indicates a need for further simplification of disjunctions. The case where the body adds conditions is a little more complicated, but similarly results in a stable value, if simplifications are applied.