Cannot have location_invariant before loop in witness

[sim642]

Leftover from #1372:

Cannot have location_invariant right before loop because we have no non-loop-head node there. This meant our existing witness tests had to be changed to loop_invariants which make more sense. But our inability to have location invariants before loops could also turn out to be problematic.

int i = 0;
// we have no node here to attach i == 0 to
while (i < 10)
  i++;