Semantics of assert statements

[salvadorer]

Hey,
I'm working with CBMC 5.95.1 and I noticed that CBMC does not add asserted conditions to the path conditions. For e.g.:

#include <assert.h>

extern int __VERIFIER_nondet_int(void);

int main() {
  int x = __VERIFIER_nondet_int();
  assert(x < 0);
  assert(x <= 0);
 }

CBMC would report a warning about both assertions but there's actually no value for x that can trigger the second assertion.

[tautschnig]

That's indeed true, see #5866: we might revisit this at some point, but until then please redefine the assert macro like this:

#undef assert
#define assert(C) __CPROVER_assert((C), "assertion"); __CPROVER_assume(C)

[martin-cs]

@salvadorer Just for interest, this is why they don't alter the path condition:

#2031
92b92d6

I'm still reasonably convinced this is the correct design decision.

[tautschnig]

Closing as this is documented behaviour.