path: root/float_test7.bpl

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