#include <inttypes.h>
// cbmc -DPREFIX=0 -DSUFFIX=0 -DTARGET=1234 -DLEN=6 collision.c
int main()
{
    uint32_t prefix=PREFIX;
    uint32_t suffix=SUFFIX;
    unsigned char str[LEN];

    uint32_t x = prefix;
    x ^= str[0] << 7;
    for(int i=0; i<LEN;i++) {
        __CPROVER_assume(str[i]<='z');
        __CPROVER_assume(str[i]>='0');
        x = (1000003*x) ^ str[i];
    }
    x ^= LEN;
    x ^= suffix;
    assert(x!=TARGET);
}