path: root/float_test5.bpl

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