diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml index 5022d6fd6adde061e50d9b15851be9c0391ad98c..ef21fe8eec6802213945ee09f9302148da42031d 100644 --- a/src/kernel_services/abstract_interp/ival.ml +++ b/src/kernel_services/abstract_interp/ival.ml @@ -882,9 +882,11 @@ let cast_float_to_int_non_nan ~signed ~size (min, max) = assert false (* impossible if min-max are correct *) let cast_float_to_int ~signed ~size iv = - match Fval.min_and_max (project_float iv) with - | Some (min, max), _nan -> cast_float_to_int_non_nan ~signed ~size (min, max) - | None, _ -> bottom (* means NaN *) + if equal top iv then top + else + match Fval.min_and_max (project_float iv) with + | Some (min, max), _nan -> cast_float_to_int_non_nan ~signed ~size (min, max) + | None, _ -> bottom (* means NaN *) (* These are the bounds of the range of integers that can be represented