1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7_Bool __VERIFIER_nondet_bool();
8
9void f(int d) {
10 int x, y, k, z = 1;
11 L1:
12 while (z < k) { z = 2 * z; }
13 __VERIFIER_assert(z>=2);
14 L2:
15 while (x > 0 && y > 0) {
16 _Bool c = __VERIFIER_nondet_bool();
17 if (c) {
18 P1:
19 x = x - d;
20 y = __VERIFIER_nondet_bool();
21 z = z - 1;
22 } else {
23 y = y - d;
24 }
25 }
26}
27
28void main() {
29 _Bool c = __VERIFIER_nondet_bool();
30 if (c) {
31 f(1);
32 } else {
33 f(2);
34 }
35}