//@ lemma aaa: \forall integer p, q; p>0 && q > 0 ==> p+q>=42;

//@ ensures bbb: \result == 42;
int foo(int x,int y) {
	x += 1;
	//@ assert ccc: x>0;
	y += 1;
	//@ assert ddd: y>0;
	return x+y;
}