diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index cb8d0a9c2ba76e3fe76a6e7ff3c9f2085d95fb0a..a6eb3d32bead52571d35d58dfe6fd631b93c04c8 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -415,10 +415,12 @@ let cardinal_zero_or_one t =
 let diff v _ = `Value v
 let diff_if_one v _ = `Value v
 
-let fold_int f t acc =
+let fold_int ?(increasing=true) f t acc =
   match t.min, t.max with
   | None, _ | _, None -> raise Error_Top
-  | Some inf, Some sup -> Int.fold f ~inf ~sup ~step:t.modu acc
+  | Some inf, Some sup ->
+    let step = if increasing then t.modu else Int.neg t.modu in
+    Int.fold f ~inf ~sup ~step acc
 
 let fold_enum f v acc =
   fold_int (fun x acc -> f (inject_singleton x) acc) v acc
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
index b3854e42dfbeacd878f599c315188284d3ce80e3..1ff9f2500762b8cd68048f483e63c7041dcf0a05 100644
--- a/src/kernel_services/abstract_interp/int_interval.mli
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -87,4 +87,4 @@ val subdivide: t -> t * t
 val reduce_sign: t -> bool -> t or_bottom
 val reduce_bit: int -> t -> bool -> t or_bottom
 
-val fold_int: (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
+val fold_int: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 6c04167b945f26f10de6e6881f87166653d19a20..c1703533b426490b30ef7003a16b11e0a5ce3237 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -148,7 +148,10 @@ let for_all f (a : Integer.t array) =
 let exists = Extlib.array_exists
 
 let iter = Array.iter
-let fold = Array.fold_left
+let fold ?(increasing=true) =
+  if increasing
+  then fun f array acc -> Array.fold_left (fun acc x -> f x acc) acc array
+  else Array.fold_right
 
 let truncate_no_bottom r i =
   assert (i > 0);
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index 3743502d0310cf10342229f97568f34954a350f3..e099a841d7cb19194df2412bf458d1841dc07f85 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -75,7 +75,7 @@ val cardinal: t -> int
 val for_all: (Integer.t -> bool) -> t -> bool
 val exists: (Integer.t -> bool) -> t -> bool
 val iter: (Integer.t -> unit) -> t -> unit
-val fold: ('a -> Integer.t -> 'a) -> 'a -> t -> 'a
+val fold: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
 val map: (Integer.t -> Integer.t) -> t -> t
 val filter: (Integer.t -> bool) -> t -> t or_bottom
 val map_reduce: (Integer.t -> 'a) -> ('a -> 'a -> 'a) -> t -> 'a
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index e5c430492205ebd7f21d573695b637f68d4f2836..2ddd8d67ac3d5f2b4387bded856aa661f63bece6 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -192,12 +192,12 @@ let make_top_from_set s =
   let min = Int_set.min s in
   let modu =
     Int_set.fold
-      (fun acc x ->
+      (fun x acc ->
          if Int.equal x min
          then acc
          else Int.pgcd (Int.sub x min) acc)
-      Int.zero
       s
+      Int.zero
   in
   let rem = Int.e_rem min modu in
   let max = Some (Int_set.max s) in
@@ -243,10 +243,10 @@ let contains_non_zero = function
   | Itv _ -> true (* at least two values *)
   | Set _ as s -> not (is_zero s)
 
-let fold_int f v acc =
+let fold_int ?(increasing=true) f v acc =
   match v with
-  | Itv i -> Int_interval.fold_int f i acc
-  | Set s -> Int_set.fold (fun acc x -> f x acc) acc s
+  | Itv i -> Int_interval.fold_int ~increasing f i acc
+  | Set s -> Int_set.fold ~increasing f s acc
 
 let fold_enum f v acc = fold_int (fun x acc -> f (inject_singleton x) acc) v acc
 
@@ -385,8 +385,8 @@ let join v1 v2 =
       let l = Int_set.cardinal s in
       if l = 0 then t
       else
-        let f modu elt = Int.pgcd modu (Int.abs (Int.sub r elt)) in
-        let modu = Int_set.fold f modu s in
+        let f elt modu = Int.pgcd modu (Int.abs (Int.sub r elt)) in
+        let modu = Int_set.fold f s modu in
         let rem = Int.e_rem r modu in
         let min = match min with
             None -> None
@@ -527,9 +527,9 @@ let div x y =
   match y with
   | Set sy ->
     Int_set.fold
-      (fun acc elt ->
+      (fun elt acc ->
          Bottom.join join acc (scale_div_or_bottom ~pos:false elt x))
-      `Bottom sy
+      sy `Bottom
   | Itv iy -> Int_interval.div (make_range x) iy >>-: inject_itv
 
 (* [scale_rem ~pos:false f v] is an over-approximation of the set of
@@ -550,10 +550,10 @@ let c_rem x y =
     match x with
     | Set xx -> inject_set_or_top_or_bottom (Int_set.c_rem xx yy)
     | Itv _ ->
-      let f acc y =
+      let f y acc =
         Bottom.join join (scale_rem_or_bottom ~pos:false y x) acc
       in
-      Int_set.fold f `Bottom yy
+      Int_set.fold f yy `Bottom
 
 (** Computes [x (op) ({y >= 0} * 2^n)], as an auxiliary function for
     [shift_left] and [shift_right]. [op] and [scale] must verify
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 4d8d0c7d9e3654c42bd7a0a7b512c37f916c7c9d..69160f90d05ea983dadbdc4fda9ef5ad9cddb97a 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -173,9 +173,10 @@ val all_values: size:Integer.t -> t -> bool
 
 val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool
 
-(** Iterates on all integers represented by an abstraction.
+(** Iterates on all integers represented by an abstraction, in increasing order
+    by default. If [increasing] is set to false, iterate by decreasing order.
     @raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
-val fold_int: (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
+val fold_int: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
 
 (** Low-level operation for demarshalling *)
 val rehash: t -> t
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 0d957509785667ab23be58bf1defbe5af0dc2f3d..a0601a432396347902a0cd2058a4f81537b5fc3b 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -398,6 +398,12 @@ let fold_int f v acc =
   | Float _ -> raise Error_Top
   | Int i -> Int_val.fold_int f i acc
 
+let fold_int_decrease f v acc =
+  match v with
+  | Bottom -> acc
+  | Float _ -> raise Error_Top
+  | Int i -> Int_val.fold_int ~increasing:false f i acc
+
 let fold_enum f v acc =
   match v with
   | Bottom -> acc
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index 2e179f6f6086965770c256bee127320a8a5de988..7a7d85dd7e224557e856543a7a21d59705b21737 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -187,6 +187,11 @@ val fold_int : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
     Raise {!Abstract_interp.Error_Top} if the argument is a float or a
     potentially infinite integer. *)
 
+val fold_int_decrease : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
+(** Iterate on the integer values of the ival in decreasing order.
+    Raise {!Abstract_Interp.Error_Top} if the argument is a float or a
+    potentially infinite integer. *)
+
 val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a
 (** Iterate on every value of the ival. Raise {!Abstract_intrep.Error_Top} if
     the argument is a non-singleton float or a potentially infinite integer. *)