/*@
  requires \valid_read(arr + (0 .. 3));
  assigns \nothing;
*/
int foo(const int arr[const static 4]) {
	const unsigned int h = 7 & 0b11;
	//@ assert 0 <= h < 4;
	const int hvalue = arr[h];

	const unsigned int i = 7 % 4;
	//@ assert 0 <= i < 4;
	const int ivalue = arr[i];

	/*@
	  loop invariant 0 <= s <= 8;
	  loop assigns s;
	  loop variant 8 - s;
	*/
	for (unsigned int s = 0; s < 8; s += 1) {
		const unsigned int j = s & 0b11;
		//@ assert 0 <= j < 4;
		const int jvalue = arr[j];

		const unsigned int k = s % 4;
		//@ assert 0 <= k < 4;
		const int kvalue = arr[k];
	}

	return 0;
}

/*@
  assigns \nothing;
*/
int main(void) {
	const int arr[4] = {0, 1, 2, 3};

	const unsigned int h = 7 & 0b11;
	//@ assert 0 <= h < 4;
	const int hvalue = arr[h];

	const unsigned int i = 7 % 4;
	//@ assert 0 <= i < 4;
	const int ivalue = arr[i];

	/*@
	  loop invariant 0 <= s <= 8;
	  loop assigns s;
	  loop variant 8 - s;
	*/
	for (unsigned int s = 0; s < 8; s += 1) {
		const unsigned int j = s & 0b11;
		//@ assert 0 <= j < 4;
		const int jvalue = arr[j];

		const unsigned int k = s % 4;
		//@ assert 0 <= k < 4;
		const int kvalue = arr[k];
	}

	foo(arr);

	return 0;
}