LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c

/*
 * Date: 2012-06-03
 * Author: heizmann@informatik.uni-freiburg.de
 *
 * 2-lex ranking function: f(k, a[k], a[0], a[1048]) = (1048 - k, a[k])
 *
 */
extern int __VERIFIER_nondet_int(void);

int main() {
	int a[1048];
	int k = 0;

  for (int i = 0; i < 1048; i++) {
    a[i] = __VERIFIER_nondet_int();
  }

	while (k < 1048 && a[k] >= 0) {
		if (__VERIFIER_nondet_int()) {
			k++;
		} else {
			a[k]--;
		}
	}
	return 0;
}