Incorrectly failing assertion in program with goto statements

[andreast271]

The example file is attached:
gotos.c.txt

The failing assertion is line 15: assert(canary). On all valid execution paths, canary == 1, so the assertion should pass.

A look at the program equation shows the problem:

$cbmc --unwind 2 --unwinding-assertions gotos.c --program-only | grep canary
(11) canary!0@1#2 == 1
(14) canary!0@2#2 == 1
(18) ASSERT(!(canary!0@2#0 == 0))

The level 2 version of variable canary in the assertion is not the one in the program equation. At a guess the mechanism keeping track of scopes gets confused by the goto statements that is crossing scope boundaries.
Note: the example originated as an auto-generated C file created by Csmith.

CBMC version: 6.2.0
Operating system: Linux 64
Exact command line resulting in the issue: cbmc --unwind 2 --unwinding-assertions gotos.c
What behaviour did you expect: all assertions should pass
What happened instead: one assertion failed

[tautschnig]

Thank you for the very helpful report! Proposed fix in #8439.