1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7unsigned int __VERIFIER_nondet_uint();
8_Bool __VERIFIER_nondet_bool();
9
10int main()
11{
12 unsigned int x1=__VERIFIER_nondet_uint(), x2=__VERIFIER_nondet_uint(), x3=__VERIFIER_nondet_uint();
13 unsigned int d1=1, d2=1, d3=1;
14 _Bool c1=__VERIFIER_nondet_bool(), c2=__VERIFIER_nondet_bool();
15
16 while(x1>0 && x2>0 && x3>0)
17 {
18 if (c1) x1=x1-d1;
19 else if (c2) x2=x2-d2;
20 else x3=x3-d3;
21 c1=__VERIFIER_nondet_bool();
22 c2=__VERIFIER_nondet_bool();
23 }
24
25 __VERIFIER_assert(x1==0 || x2==0 || x3==0);
26 return 0;
27}