You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
CBMC version: 5.42.0 (cbmc-5.42.0-2-g038a53b50)
Operating system: Debian
Exact command line resulting in the issue: goto-instrument --unwind 3 --unwinding-assertions test.gb test-unwinding.gb && cbmc test-unwinding.gb --function foo
What behaviour did you expect: No assertion failures
What happened instead: Two assertion failure
I have the following code in test.c:
int foo() {
while (1) {
}
__CPROVER_assert(0, "reachable");
}
When I run cbmc --unwind 3 --unwinding-assertions test.c --function foo, I don't see any assertion failures:
[foo.assertion.1] line 4 reachable: SUCCESS
** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL
Now I try to do the same thing with goto-instrument:
[foo.1] line 2 assertion: FAILURE
[foo.assertion.1] line 4 reachable: FAILURE
** 2 of 2 failed (2 iterations)
VERIFICATION FAILED
The behavior I want is actually what cbmc does, which is to essentially treat the loop as assume(false). Why does goto-instrument behave differently, and is it intended to behave differently?