extern void __VERIFIER_error() __attribute__ ((__noreturn__));
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
extern void __VERIFIER_assume(int);
//#define SIZE 100000
int __VERIFIER_nondet_int();
int main()
{
    int SIZE;
    __VERIFIER_assume(SIZE>0);
	int k;

	int i;
	int a[SIZE];
	int b[SIZE];
	int c[SIZE];

	//init and update
	for (i = 0; i < SIZE; i++)
	{
		int q = __VERIFIER_nondet_int();
		a[i] = 0;
		if (q == 0)
		{
			a[i] = 1;
			b[i] = i % 2;
		}
		if (a[i] != 0)
		{
			if (b[i] == 0)
			{
				c[i] = 0;
			}
			else
			{
				c[i] = 1;
			}
		}
	}

    __VERIFIER_assume(k>=0 && k<SIZE && k>=SIZE/2);
	a[k] = 1;

	for (i = 0; i < SIZE; i++)
	{
		if(i==k)
		{
			__VERIFIER_assert(a[i] != 1); 
		}
	}
	return 0;
}

