path: root/float_test3.bpl

 procedure F() returns () {
	assert fp(5) == fp(5 8 23);
}