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