fix(arith): Do not expose unnormalized intervals in only_borne_XXX (#…

…1081)

The `only_borne_sup` and `only_borne_inf` functions have been introduced
in 0968433 and are intended to only
take in consideration upper and lower bounds of an interval,
respectively.

These functions work by replacing the lower (resp. upper) bound of
each interval in an union by negative (resp. positive) infinities,
leading to bogus and non-normalized representations; for instance,
computing `only_borne_inf` on the union (which we will assume is
normalized, i.e. a < b < c < d):

  [a, b] U [c, d]

returns

  [a, +oo[ U [c, +oo[

which should be just

  [a, +oo[

This does not cause issues currently because we always ultimately call
`borne_sup` (resp. `borne_inf`) on these, but these functions should not
return such bogus intervals in the first place.

This patch changes functions `only_borne_sup` and `only_borne_inf` to
only return the last (resp. first) interval in the union, ensuring that
their result is always a single normalized interval without change of
semantics.

src/lib/reasoners/intervals.ml

@@ -133,18 +133,22 @@ let borne_inf = function
   | { ints = (Strict (v, ex), _) :: _; _ } -> v, ex, false
   | _ -> raise No_finite_bound
 
-let only_borne_inf ({ ints; _ } as t) =
-  { t with ints = List.map (function (inf, _) -> (inf, Pinfty)) ints; }
+let only_borne_inf = function
+  | { ints = (inf, _) :: _ ; _ } as t -> { t with ints = [(inf, Pinfty)] }
+  | _ -> assert false
 
 let borne_sup { ints; _ } =
   match List.rev ints with
   | (_, Large (v, ex))::_ -> v, ex, true
   | (_, Strict (v, ex))::_ -> v, ex, false
   | _ -> raise No_finite_bound
 
-let only_borne_sup ({ ints; _ } as t) =
-  { t with ints = List.map (function (_, sup) -> (Minfty, sup)) ints; }
-
+let only_borne_sup t =
+  let rec aux = function
+    | [] -> assert false
+    | [ (_, sup) ] -> { t with ints = [(Minfty, sup)] }
+    | _ :: tl -> aux tl
+  in aux t.ints
 
 let explain_borne = function
   | Large (_, e) | Strict (_, e) -> e