`for` loop invariant location in YAML witness

[sim642]

As pointed out by Freiburg, our YAML witnesses put for loop invariants after the for keyword, but before the for loop initializer.
A more conventional location would be before the for keyword.