path: root/float_test5.bpl

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