Dear all,
it seems like cbmc misses an assertion violation in the program:
#include <assert.h>
extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);
int main() {
int z = __VERIFIER_nondet_int();
int k = __VERIFIER_nondet_int();
__VERIFIER_assume(1 < z);
__VERIFIER_assume(1 <= z && k <= 1);
assert(0);
}
Calling "cbmc test.c" gives:
** Results:
test.c function main
[main.assertion.1] line 9 assertion 0: SUCCESS
but clearly the assertion is reachable.
CBMC version: 5.93.0
Operating system: Ubuntu
Dear all,
it seems like cbmc misses an assertion violation in the program:
Calling "cbmc test.c" gives:
** Results:
test.c function main
[main.assertion.1] line 9 assertion 0: SUCCESS
but clearly the assertion is reachable.
CBMC version: 5.93.0
Operating system: Ubuntu