Model.evaluate on FloatingPointFormula does not exist.
There is a generic Model.evaluate(Formula) method that returns an Object. For Z3, this seems to be a Rational when passing a FloatingPointFormula (by first converting to reals).

Is this is an oversight or are there underlying issues that make it hard to provide an evaluate method that always return Rational?