path: root/float_test3.bpl

 procedure F() returns () {
	var x : float;
	var y : float;
	y := x - x;
	assert y == x;
}