__CPROVER_assume doesn't work as expected with large constant

[HclX]

CBMC version: CBMC version 5.56.0 (cbmc-5.56.0) 64-bit x86_64 linux
Operating system: Linux
Exact command line resulting in the issue: cbmc test.c --function cbmc_entry
What behaviour did you expect: with the following test code, I'm expecting the first assertion succeeds and the second one fails

#include <stdint.h>
#include <stddef.h>
#include <assert.h>

void cbmc_entry() {
    size_t x0 = nondet_size_t();
    size_t x1;

    __CPROVER_assume(x0 == 0x82002060);

    if (x0 == 0x82002060) {
        x1 = 1000;
    } else {
        x1 = 1001;
    }
    assert(x1 == 1000);
    assert(x1 == 1001);
}

What happened instead: both assertions are tested success

** Results:
test.c function cbmc_entry
[cbmc_entry.assertion.1] line 16 assertion x1 == 1000: SUCCESS
[cbmc_entry.assertion.2] line 17 assertion x1 == 1001: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

[HclX]

However, if I change the constant from 0x82002060 to 0x7fffffff, it behaves as expected. This seems to have something do with signed/unsigned conversion for constants.

[kroening]

The function nondet_size_t needs to be declared. Add
size_t nondet_size_t();
and you get the expected result.

[xx24678]

I see. I think the documentation is a little bit confusing. It should probably not use the type in the function name in the example and emphasize that this function needs to be declared.

[tautschnig]

@xx24678 Would you mind providing a pointer to the documentation that you would like to see us improve? Also, CBMC does say file test.c line 6 function cbmc_entry: function 'nondet_size_t' is not declared, but perhaps this isn't sufficient?

[xx24678]

Here is the instructions from current user manual:

When desired, nondeterminism can be introduced explicitly into the program by means of functions that begin with the prefix nondet_. As an example, the following function returns a nondeterministically chosen unsigned short int:

unsigned short int nondet_ushortint();
Note that the body of the function is not defined. The name of the function itself is irrelevant (save for the prefix), but must be unique. Also note that a nondeterministic choice is not to be confused with a probabilistic (or random) choice.

Maybe we should say something like "declaring a function without implementation" ?