Complicating it even more, if "a" is a signed-integer than the compiler will assume that statement holds and optimize accordingly, put your correctness prover would instead need to flag that (or add the caveat that a < INT_MAX)