Invariant violation during goto conversion on C file with goto statements

[andreast271]

label.c.txt

With the attached C file label.c, CBMC will fail during goto conversion with an invariant violation.
Specifically:

$ cbmc label.c 
CBMC version 6.2.0 (cbmc-6.2.0-dirty) 64-bit x86_64 linux
Type-checking label
Generating GOTO Program
--- begin invariant violation report ---
Invariant check failed
File: goto-conversion/goto_convert.cpp:351 function: finish_gotos
Condition: false
Reason: Unreachable

The file looks rather nonsensical. It started as an auto-generated C file (via Csmith). As far as I can tell it contains legal C and should not cause a crash.

CBMC version: 6.2.0
Operating system: Liunx x86_64
Exact command line resulting in the issue: cbmc label.c
What behaviour did you expect: cbmc to not crash
What happened instead: invariant violation

[tautschnig]

Thank you, we seem to have carried this bug since 2017. Fix in #8438.