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 int v;
22 unsigned int v1;
23 unsigned int v2;
24 char parity1;
25 char parity2;
26 v1 = v;
27 parity1 = (char)0;
28 while (v1 != 0) {
29 if (parity1 == (char)0) {
30 parity1 = (char)1;
31 } else {
32 parity1 = (char)0;
33 }
34 v1 = v1 & (v1 - 1U);
35 }
36 v2 = v;
37 parity2 = (char)0;
38 v2 = v2 ^ (v2 >> 1u);
39 v2 = v2 ^ (v2 >> 2u);
40 v2 = (v2 & 286331153U) * 286331153U;
41 if (((v2 >> 28u) & 1u) == 0) {
42 parity2 = (char)0;
43 } else {
44 parity2 = (char)1;
45 }
46 __VERIFIER_assert(parity1 == parity2);
47 return 0;
48}