path: root/float_test3.bpl

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