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 n;
22 unsigned int s;
23 unsigned int d;
24 unsigned int m;
25 d = (1 << s) - 1;
26 if (d > 0) {
27 m = n;
28 while (n > d) {
29 m = 0;
30 while (n > 0) {
31 m += n & d;
32 n = n >> s;
33 }
34 n = m;
35 }
36 if (m == d) {
37 m = 0;
38 }
39 __VERIFIER_assert(m == n % d);
40 }
41 return 0;
42}