CBMC gives spurious warning for unwind bound > 1

[Costandre97]

CBMC seems to produce some weirdly inconsistent results for the following program:

#define ASSERT(cond) __CPROVER_assert((cond), "assertion"); __CPROVER_assume(cond)      
typedef struct  { int id; } test;
int main(int argc, char *argv) {
start:;
test test0 = {0};
__CPROVER_assume(argc > 0);
if(argv[0]){
// ASSERT(0);
ASSERT(test0.id == argc); //line 9, should always fail
goto start;
}
ASSERT(test0.id != 6); //line 12, should always succeed
return 0;
}

Running CBMC with default options causes it to (incorrectly) report the assertion on line 12 as failing.
However if I simplify the (unrelated) assertion on line 9 to ASSERT(0), the result is correct.
Similarly if I manually set it to unwind once (cbmc --unwind 1) the result is correct.
Setting a higher bound causes the error to appear again.

Version: CBMC version 6.6.0 (cbmc-6.6.0-14-g34dc8dcdf0) 64-bit x86_64 linux
Built from 34dc8dc

[tautschnig]

Thank you for your report. We need to review why the declaration after the label causes this misbehaviour.