cbmc?: Bitvectors complicated

[chkl]

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
extern unsigned short __VERIFIER_nondet_ushort(void);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
extern void __assert_fail(const char * __assertion,
                          const char * __file,
                          unsigned int __line,
                          const char * __function) __attribute__((__nothrow__,__leaf__,__noreturn__));
extern void __assert_perror_fail(int __errnum,
                                 const char * __file,
                                 unsigned int __line,
                                 const char * __function) __attribute__((__nothrow__,__leaf__,__noreturn__));
extern void __assert(const char * __assertion,
                     const char * __file,
                     int __line) __attribute__((__nothrow__,__leaf__,__noreturn__));
int main()
{
    unsigned short x = __VERIFIER_nondet_ushort();
    unsigned short y = __VERIFIER_nondet_ushort();
    unsigned int xx;
    unsigned int yy;
    unsigned int zz;
    unsigned int z = 0;
    unsigned int i = 0;
    while (i < sizeof(x) * 8)
    {
        __VERIFIER_assert((x & 1u << i) != 6);
        z |= (x & 1u << i) << i | (y & 1u << i) << i + 1;
        i += 1u;
    }
    xx = x;
    yy = y;
    xx = (xx | xx << 8u) & 16711935u;
    xx = (xx | xx << 4u) & 252645135u;
    xx = (xx | xx << 2u) & 858993459u;
    xx = (xx | xx << 1u) & 1431655765u;
    yy = (yy | yy << 8u) & 16711935u;
    yy = (yy | yy << 4u) & 252645135u;
    yy = (yy | yy << 2u) & 858993459u;
    yy = (yy | yy << 1u) & 1431655765u;
    zz = xx | yy << 1u;
    __DUMMY_VERIFIER_assert(z == zz);
}

I have no idea what the correct answer is, but the verdicts are as follows: sea/ultimate : sat klee: unknown cbmc/smack/cpachecker: unsat

[chkl]

extern void __VERIFIER_error() __attribute__((__noreturn__));
extern unsigned short __VERIFIER_nondet_ushort(void);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int main()
{
    unsigned short x = __VERIFIER_nondet_ushort();
    unsigned int i = 0;
    while (i < sizeof(x) * 8)
    {
        __VERIFIER_assert((x & (1 << i)) != 6);
        i++;
    }
}

[chkl]

klee also says unsat (after defining the shim for __VERIFIER_nondet_ushort()).

I also believe that this is "unsat", because (1>>i) should always be a power of 2 or 0 and therefore that expression should always be 1 or 0.

EDIT: Not true, bit shifting by a number of bits that it is greater than the bitsize of the datatype is undefined behavior. So it actually is Sat.

[wuestholz]

@chkl Yes, that sounds right.