path: root/float_test4.bpl

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