namespace;
include rt;

// a loop proof only holds while the body leaves the index alone: here the body
// moves i back below 0 once, so t[i] keeps its check and the access faults
int main() {
	int[4] t; int s = 0, once = 1;
	for (int i = 0; i < 4; i++) { s = s + t[i]; if (once) { once = 0; i = -3000; } }
	rt.put_n(s); rt.put_c(10);
	return 0;
}