Output location invariants for witnesses at labels #1735
Description
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.