/* VERIFY_OPTS: --symbolic --sequential -o ignore:integer */ /* TAGS: sym c */ /* NB. The ignore:integer is a workaround for --symbolic also running a * concrete computation (which does not follow path constraints), in which the * divisor happens to be zero... */ #include extern void __VERIFIER_assert(int); signed char gcd_test(signed char a, signed char b) { signed char t; if (a < 0) a = -a; if (b < 0) b = -b; while (b != 0) { t = b; b = a % b; a = t; } return a; } extern char __VERIFIER_nondet_char(void); int main() { signed char x = __VERIFIER_nondet_char(); signed char y = __VERIFIER_nondet_char(); signed char g; if (y > 0 && x % y == 0) { g = gcd_test(x, y); __VERIFIER_assert(g == y); } return 0; }