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