1extern int nondet_int(void);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8
9extern void __assert_fail (__const char *__assertion, __const char *__file,
10 unsigned int __line, __const char *__function)
11 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
12extern void __assert_perror_fail (int __errnum, __const char *__file,
13 unsigned int __line,
14 __const char *__function)
15 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
16extern void __assert (const char *__assertion, const char *__file, int __line)
17 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
18
19int main()
20{
21 unsigned short x;
22 unsigned short y;
23 unsigned int xx;
24 unsigned int yy;
25 unsigned int zz;
26 unsigned int z = 0;
27 unsigned int i = 0;
28 while (i < 32U) {
29 z |= ((x & (1U << i)) << i) | ((y & (1U << i)) << (i + 1));
30 i += 1U;
31 }
32 xx = x;
33 yy = y;
34 xx = (xx | (xx << 8u)) & 16711935U;
35 xx = (xx | (xx << 4u)) & 252645135U;
36 xx = (xx | (xx << 2u)) & 858993459U;
37 xx = (xx | (xx << 1u)) & 1431655765U;
38 yy = (yy | (yy << 8u)) & 16711935U;
39 yy = (yy | (yy << 4u)) & 252645135U;
40 yy = (yy | (yy << 2u)) & 858993459U;
41 yy = (yy | (yy << 1u)) & 1431655765U;
42
43 zz = xx | (yy << 1U);
44
45 __VERIFIER_assert(z == zz);
46}