1extern void __VERIFIER_assume(int);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8int __VERIFIER_nondet_int();
9_Bool __VERIFIER_nondet_bool();
10
11main()
12{
13 int x=__VERIFIER_nondet_int();
14 int y=__VERIFIER_nondet_int();
15 int z=__VERIFIER_nondet_int();
16 __VERIFIER_assume(x<100);
17 __VERIFIER_assume(z<100);
18 while(x<100 && 100<z)
19 {
20 _Bool tmp=__VERIFIER_nondet_bool();
21 if (tmp)
22 {
23 x++;
24 }
25 else
26 {
27 x--;
28 z--;
29 }
30 }
31
32 __VERIFIER_assert(x>=100 || z<=100);
33}