path: root/float_test4.bpl

 procedure F() returns () {
	var x : float;
	x := fp (.5 8 23);
	assert x == fp (-1 0);
}