From 36e3bafc5ea16c9d42c86f5e3caa7d92e0c0001d Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 7 Oct 2021 17:57:29 +0200
Subject: [PATCH] [e-acsl:typing] fix bug for \prod in one corner case
---
src/plugins/e-acsl/src/analyses/interval.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 61dc1cd07a7..04724d513b5 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,
--
GitLab