[JVM] Saturate FP casts at rounded integral upper bounds

[CaelmBleidd]

Java floating-point casts at a rounded integral upper bound currently enter an out-of-range SMT fp.to_sbv conversion. Its result cannot be evaluated in the cached model, so a later branch crashes with both trueModels/falseModels empty. This reproduces in real ComplexFormat analysis through the Fraction(double, double, int, int) constructor.

Saturate equality to the signed integral maximum before the SMT conversion. Java requires float -> int at 2^31, and float/double -> long at 2^63, to return MAX_VALUE. The fork policy is unchanged.

Validation: three ordinary Java source regressions reproduce the same fork failure before the fix and all three pass afterward. Each test checks both the boundary and the other input branch. No full test suite was run.