void foo(void) {
	//@ loop invariant s == 0;
	while (true)
	{
		int s = 0;
	}
}