path: root/float_test6.bpl

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