procedure F() returns () {
	var x : float;
	var y : float;
	assert x + y == fp(0);
}