path: root/float_test5.bpl

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