Output location invariants for witnesses at labels

[sim642]

For SV-COMP correctness witnesses we only output loop invariants. For goto-based loops, we output nothing.

Following Matthias Heizmann's proposal, we should also output location invariants at labels. So goto-based loops would also have an an invariant at least one point.