An expression that modifies an LValue is said to be invertible w.r.t. the
LValue if we can write an expression in terms of the original value of the
LValue before the modification. For example, the expression x + 1 is invertible
w.r.t x because we can write this expression in terms of the original value of
x which is (x - 1) + 1.

In this PR, we use invertibility of statements to support bounds widening in
loops. More specifically, if a statement modifies a variable that occurs in the
bounds expression of a null-terminated array then instead of killing its bounds
at that statement we use invertibility of the statement to try to write the
widened bounds in terms of the original value of the variable.