//#Safe
// 27.06.16: Handling of unary minus 

procedure ULTIMATE.start()
{
	var x, y, z : int;

	assume -y + -y <= 4;
	assert y >= -2 ;

}