If we know that some predicate is true for AddRec and an invariant

(w.r.t. this AddRec's loop), this fact is, in particular, true on the first

iteration. We can try to prove the facts we need using the start value.

The motivating example is proving things like

isImpliedCondOperands(>=, X, 0, {X,+,-1}, 0}

The initial version of the patch was reverted because it missed the check that

the predicate being proved is actually guarded by this check on 1st iteration.

If it was not executed on 1st iteration (but possibly executes after that), then

it is incorrect to use reasoning about IV start to prove it.

Added the test where the miscompile was seen. Unfortunately, my attempts

to reduce it with bugpoint did not succeed; it can further be reduced when

we understand how to do it without losing the initial bug's notion.