path: root/float_test2.bpl

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