path: root/float_test5.bpl

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