path: root/float_test2.bpl

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