1extern int nondet_int(void);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8long gcd_test(long a, long b)
9{
10 if (a < 0) a = -a;
11 if (b < 0) b = -b;
12
13 if (a == 0) {
14 return b;
15 }
16
17 while (b != 0) {
18 if (a > b) {
19 a = a - b;
20 } else {
21 b = b - a;
22 }
23 }
24 return a;
25}
26
27
28int main()
29{
30 long x;
31 long y;
32 long g;
33
34 x = 63;
35 y = 18;
36
37 g = gcd_test(x, y);
38
39 __VERIFIER_assert(x % g == 0);
40 __VERIFIER_assert(y % g == 0);
41 __VERIFIER_assert(g == 9);
42
43 return 0;
44}