path: root/float_test8.bpl

procedure F() returns () {
	assert fp(-oo)==fp(-oo);
}