diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml index 391bc645b63dc7bf3392a403e1226347821f9544..60c93219ceb3b745bb32c60e06766b1a7c445b72 100644 --- a/src/kernel_services/abstract_interp/ival.ml +++ b/src/kernel_services/abstract_interp/ival.ml @@ -2908,7 +2908,8 @@ struct match result_size v1 v2 ~s1 ~s2 () with | None -> (* Unbounded result *) - None + if lower && s = Off then Some Int.zero + else if not lower && s = On then Some Int.minus_one else None | Some n -> (* The result is bounded: iterate from the rightmost significant bit *) let rec step r v1 v2 i =