1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7
8int __VERIFIER_nondet_bool();
9
10void foo()
11{
12 int y=0;
13 int c1=__VERIFIER_nondet_bool(), c2=__VERIFIER_nondet_bool();
14 if (c1) y++;
15 if (c2) y--;
16 else y+=10;
17}
18
19int main()
20{
21 int d = 1;
22 int x;
23 int c1=__VERIFIER_nondet_bool(), c2=__VERIFIER_nondet_bool();
24
25 if (c1) d = d - 1;
26 if (c2) foo();
27
28 c1=__VERIFIER_nondet_bool(), c2=__VERIFIER_nondet_bool();
29
30 if (c1) foo();
31 if (c2) d = d - 1;
32
33 while(x>0)
34 {
35 x=x-d;
36 }
37
38 __VERIFIER_assert(x<=0);
39}