diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml index 61dc1cd07a785516a3e6d3d19585b61a90a18282..04724d513b504014bc702496717c082f8bc61dc4 100644 --- a/src/plugins/e-acsl/src/analyses/interval.ml +++ b/src/plugins/e-acsl/src/analyses/interval.ml @@ -617,7 +617,7 @@ let infer_sum_product oper lambda min max = match lambda, min, max with Extlib.opt_map2 (fun m max -> match max_lambda with - | Some ml when Z.lt ml Z.zero -> + | Some ml when Z.lt ml Z.zero && not (Z.equal m Z.one) -> (* when [lambda] is necessarily negative with an odd number of iterations (>1), the result is necessarily negative, so smaller than the maximal (positive) value. Therefore,