namespace;
include rt;

// a loop test i < K with a constant K proves the index of a fixed array of at
// least K elements, so the bounds check is dropped: the checked loop compiles
// to exactly as many words as the unbounded one. a variable bound proves
// nothing and keeps the check. sizes come from the functions' line blocks.
int[8] t;
int konst() { int i, s = 0; for (i = 0; i < 8; i++) s = s + t[i]; return s; }
unbounded int bare() { int i, s = 0; for (i = 0; i < 8; i++) s = s + t[i]; return s; }
int vary(int n) { int i, s = 0; for (i = 0; i < n; i++) s = s + t[i]; return s; }
unbounded int vbare(int n) { int i, s = 0; for (i = 0; i < n; i++) s = s + t[i]; return s; }

int size(word f) { word b = rt.line_block_of(f); return b[2] - b[1]; }

int main() {
	rt.put_n(konst() + bare() + vary(8) + vbare(8)); rt.put_c(10);
	rt.put_n(size(konst) == size(bare)); rt.put_c(10);
	rt.put_n(size(vary) > size(vbare)); rt.put_c(10);
	return 0;
}