With this example: cbmc --bounds-check test.c test.c function main [main.array_bounds.1] line 6 array 'a' upper bound in a[(signed long int)i]: SUCCES

With this example: cbmc --bounds-check test.c test.c function main [main.array_bounds.1] line 6 array 'a' upper bound in a[(signed long int)i]: SUCCESS [main.array_bounds.2] line 8 array 'a' upper bound in a[(signed long int)i]: FAILURE ** 1 of 2 failed (2 iterations) VERIFICATION FAILED gcc and clang both failed to find anything at compile-time.