Merge PR #11362: Lia bugfix 11191

Reviewed-by: maximedenes

1 files changed, 19 insertions, 0 deletions

diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 03f042647c..160b492d3d 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -140,6 +140,25 @@ let saturate p f sys =
     Printexc.print_backtrace stdout;
     raise x
 
+let saturate_bin (f : 'a -> 'a -> 'a option) (l : 'a list) =
+  let rec map_with acc e l =
+    match l with
+    | [] -> acc
+    | e' :: l' -> (
+      match f e e' with
+      | None -> map_with acc e l'
+      | Some r -> map_with (r :: acc) e l' )
+  in
+  let rec map2_with acc l' =
+    match l' with [] -> acc | e' :: l' -> map2_with (map_with acc e' l) l'
+  in
+  let rec iterate acc l' =
+    match map2_with [] l' with
+    | [] -> List.rev_append l' acc
+    | res -> iterate (List.rev_append l' acc) res
+  in
+  iterate [] l
+
 open Num
 open Big_int