cbmc misses an error

[salvadorer]

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

[tautschnig]

Thank you for this bug report! We end up rewriting __VERIFIER_assume(1 <= z && k <= 1); to assume(z == 1), I am trying to figure out why this is happening.