diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml index 1b36c133b57ba3063b303f5fbb9768d2889a5cb3..60c1c969c402fb6221d716482b743b1248aa650c 100644 --- a/src/kernel_services/abstract_interp/int_val.ml +++ b/src/kernel_services/abstract_interp/int_val.ml @@ -190,16 +190,15 @@ let inject_set_or_top_or_bottom = function (* Computes [min], [max], [rem] and [modu] from an integer set. *) let make_top_from_set s = let min = Int_set.min s in - let modu = - Int_set.fold - (fun x acc -> - if Int.equal x min - then acc - else Int.pgcd (Int.sub x min) acc) - s - Int.zero + let rem, modu = + if Int_set.cardinal s = 1 + then Int.zero, min + else + let modu = + Int_set.fold (fun x acc -> Int.pgcd (Int.sub x min) acc) s Int.zero + in + Int.e_rem min modu, modu in - let rem = Int.e_rem min modu in let max = Some (Int_set.max s) in let min = Some min in min, max, rem, modu diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli index 69160f90d05ea983dadbdc4fda9ef5ad9cddb97a..2f760b0c025d45340e1c81599e018c70ddd5d4cb 100644 --- a/src/kernel_services/abstract_interp/int_val.mli +++ b/src/kernel_services/abstract_interp/int_val.mli @@ -86,8 +86,7 @@ val max_int: t -> Integer.t option val min_and_max: t -> Integer.t option * Integer.t option (** Returns [min, max, rem, modu] such that for all integers [i] represented by - the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu]. - The abstraction must not be a singleton. *) + the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu]. *) val min_max_rem_modu: t -> Integer.t option * Integer.t option * Integer.t * Integer.t