Skip to content
Snippets Groups Projects
Commit 36e3bafc authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:typing] fix bug for \prod in one corner case

parent 9a9028de
No related branches found
No related tags found
No related merge requests found
...@@ -617,7 +617,7 @@ let infer_sum_product oper lambda min max = match lambda, min, max with ...@@ -617,7 +617,7 @@ let infer_sum_product oper lambda min max = match lambda, min, max with
Extlib.opt_map2 Extlib.opt_map2
(fun m max -> (fun m max ->
match max_lambda with 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 (* when [lambda] is necessarily negative with an odd number
of iterations (>1), the result is necessarily negative, of iterations (>1), the result is necessarily negative,
so smaller than the maximal (positive) value. Therefore, so smaller than the maximal (positive) value. Therefore,
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment