diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml index 2798531dc977e569afe25eb37dba840becab85d7..3fcdc8e37c7a50e030b5a3b6f717d3e343811cc1 100644 --- a/src/plugins/e-acsl/interval.ml +++ b/src/plugins/e-acsl/interval.ml @@ -148,14 +148,16 @@ let lift_binop ~safe_float f i1 i2 = match i1, i2 with | FDouble -> -. Transitioning.Float.max_float, Transitioning.Float.max_float - | FLongDouble -> raise Exit + | FLongDouble -> + raise Exit in if mini >= minf && maxi <= maxf then Float(k, None) else Rational with Z.Overflow | Exit -> Rational) | None, Some _ | Some _, None -> assert false - else Rational (* sound over-approximation *) + else + Rational (* sound over-approximation *) | (Ival _ | Float _ | Rational), (Float _ | Rational) | Rational, Ival _ -> Rational