Open
Description
CBMC version: 5.75.0
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: cbmc no_loops.c --unwind 1 --unwinding-assertions
What behaviour did you expect: The assertion main.assertion.1
in the code should fail.
What happened instead: The assertion main.assertion.1
succeeds, while there's a unexpected unwinding assertion failure.
Source code:
// no_loops.c
int loop_free() {
bb0:;
int var_3 = 1;
goto bb1;
exit:;
return 10;
bb1:;
goto exit;
}
int main() {
assert(loop_free() == 0);
return 0;
}
Output:
** Results:
no_loops.c function loop_free
[loop_free.unwind.0] line 11 unwinding assertion loop 0: FAILURE
no_loops.c function main
[main.assertion.1] line 16 assertion return_value_loop_free == 0: SUCCESS
** 1 of 2 failed (2 iterations)
VERIFICATION FAILED