diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index e6267f35c0f3bc5d808ccbbac287b0c76eef3bbe..a0a4b588d4080ef8d4e996a305fcf697a9432d23 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -256,6 +256,10 @@ let opt_hash hash v = match v with
   | None -> 31179
   | Some v -> hash v
 
+let opt_map2 f x y = match x, y with
+  | None, _ | _, None -> None
+  | Some x, Some y -> Some (f x y)
+
 (* ************************************************************************* *)
 (** Booleans                                                                 *)
 (* ************************************************************************* *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 1ef17c991ac2e33786a6ca9cff42675ad0a05a8a..5b02633a1b2a8f2bfd0fa1d450a6311139fd2250 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -229,6 +229,11 @@ val the: exn:exn -> 'a option -> 'a
 val opt_hash: ('a -> int) -> 'a option -> int
 (** @since Sodium-20150201 *)
 
+val opt_map2: ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
+(** @return [f a b] if arguments are [Some a] and [Some b], orelse return
+    [None].
+    @since Frama-C+dev *)
+
 (* ************************************************************************* *)
 (** {2 Booleans} *)
 (* ************************************************************************* *)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 0cd3328d7a8dfbfa86be0b67c528bebe08236174..7581059237cfcf961bb0ff31a7b4a3a9be2f81cb 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-  E-ACSL       [2021-10-07] Support for \prod and \numof.
 -* E-ACSL       [2021-09-29] Fix translation order of the default behavior's
                 requires clauses. They are now translated before the evaluation
                 of the assumes clauses of the other behaviors.
@@ -41,7 +42,7 @@ Plugin E-ACSL <next-release>
                 (frama-c/e-acsl#170).
 -* E-ACSL       [2021-07-16] Fix crash when using some built-in labels
                 (frama-c/e-acsl#173).
--  E-ACSL       [2021-07-06] Add support for the extended quantifier \sum.
+-  E-ACSL       [2021-07-06] Support for \sum.
 -* E-ACSL       [2021-06-22] Fix a crash that occured when using certain
                 combinations of nested blocks and annotations.
 -* E-ACSL       [2021-06-16] Fix literal string replacements in function
@@ -109,7 +110,7 @@ Plugin E-ACSL 22.0 (Titanium)
 
 -* E-ACSL       [2020-11-16] Fix soundness bug when checking
                 initialization of a chunk of heap memory block.
--  E-ACSL       [2020-10-14] Add Support for Variadic generated functions in
+-  E-ACSL       [2020-10-14] Support for Variadic generated functions in
                 the AST (frama-c/e-acsl#128).
 -  E-ACSL       [2020-10-06] Add support for the `\separated` predicate.
                 (frama-c/e-acsl#31)
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index b37bb6f30daa112897e172fdfc5e023daf355a2b..770c70c1af1d699ba3e671e938cc1e6939414b90 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -176,26 +176,32 @@ in \lstinline|\\at|}
 
 \subsection*{Version \eacslplugincodename-\eacslpluginversion}
 \begin{itemize}
+\item \changeinsection{higherorder}{support for \lstinline|\\sum|,
+  \lstinline|\\prod|, and \lstinline|\\numof|}
+\end{itemize}
+ 
+\subsection*{Version Vanadium-23}
+\begin{itemize}
 \item \changeinsection{expressions}{mark logic function and predicate
   applications as implemented}
-\item \changeinsection{fn-behavior}{mark admit and check clauses as implemented}
-\item \changeinsection{loop_annot}{mark loop variants as implemented}
+\item \changeinsection{fn-behavior}{support for admit and check clauses}
+\item \changeinsection{loop_annot}{support for loop variants}
 \end{itemize}
 
 \subsection*{Version Titanium-22}
 
 \begin{itemize}
-\item \changeinsection{expressions}{support of bitwise operations}
-\item \changeinsection{aggregates}{support of logic arrays}
+\item \changeinsection{expressions}{support for bitwise operations}
+\item \changeinsection{aggregates}{support for logic arrays}
 \end{itemize}
 
 \subsection*{Version Scandium-21}
 
 \begin{itemize}
-\item \changeinsection{reals}{support of rational numbers and operations}
+\item \changeinsection{reals}{support for rational numbers and operations}
 \item \changeinsection{fn-behavior}{remove abrupt clauses from the list of
   exceptions}
-\item \changeinsection{fn-behavior}{support of \lstinline|complete behaviors|
+\item \changeinsection{fn-behavior}{support for \lstinline|complete behaviors|
   and \lstinline|disjoint behaviors|}
 \item \changeinsection{statement_contract}{remove abrupt clauses from the list
   of exceptions}
@@ -205,45 +211,45 @@ in \lstinline|\\at|}
 \subsection*{Version Potassium-19}
 
 \begin{itemize}
-\item \changeinsection{logicspec}{support of logic functions and predicates}
+\item \changeinsection{logicspec}{support for logic functions and predicates}
 \end{itemize}
 
 \subsection*{Version Argon-18}
 
 \begin{itemize}
-\item \changeinsection{at}{support of \lstinline|\\at| on purely
+\item \changeinsection{at}{support for \lstinline|\\at| on purely
 logic variables}
-\item \changeinsection{locations}{support of ranges in memory built-ins
+\item \changeinsection{locations}{support for ranges in memory built-ins
   (e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
 \end{itemize}
 
 \subsection*{Version Chlorine-20180501}
 
 \begin{itemize}
-\item \changeinsection{expressions}{support of \lstinline|\\let| binding}
+\item \changeinsection{expressions}{support for \lstinline|\\let| binding}
 \end{itemize}
 
 \subsection*{Version 0.5}
 
 \begin{itemize}
-\item \changeinsection{alloc-dealloc}{support of \lstinline|\\freeable|}
+\item \changeinsection{alloc-dealloc}{support for \lstinline|\\freeable|}
 \end{itemize}
 
 \subsection*{Version 0.3}
 
 \begin{itemize}
-\item \changeinsection{loop_annot}{support of loop invariant}
+\item \changeinsection{loop_annot}{support for loop invariant}
 \end{itemize}
 
 \subsection*{Version 0.2}
 
 \begin{itemize}
-\item \changeinsection{expressions}{support of bitwise complementation}
-\item \changeinsection{memory}{support of \lstinline|\\valid|}
-\item \changeinsection{memory}{support of \lstinline|\\block_length|}
-\item \changeinsection{memory}{support of \lstinline|\\base_addr|}
-\item \changeinsection{memory}{support of \lstinline|\\offset|}
-\item \changeinsection{dangling}{support of \lstinline|\\initialized|}
+\item \changeinsection{expressions}{support for bitwise complementation}
+\item \changeinsection{memory}{support for \lstinline|\\valid|}
+\item \changeinsection{memory}{support for \lstinline|\\block_length|}
+\item \changeinsection{memory}{support for \lstinline|\\base_addr|}
+\item \changeinsection{memory}{support for \lstinline|\\offset|}
+\item \changeinsection{dangling}{support for \lstinline|\\initialized|}
 \end{itemize}
 
 \subsection*{Version 0.1}
diff --git a/src/plugins/e-acsl/doc/refman/higherorder.tex b/src/plugins/e-acsl/doc/refman/higherorder.tex
index cc4d91104bc4afbbbb6d7307695adc33347bf5c6..838bef143f94b793f97f26306dd375dcd0080b1e 100644
--- a/src/plugins/e-acsl/doc/refman/higherorder.tex
+++ b/src/plugins/e-acsl/doc/refman/higherorder.tex
@@ -1,8 +1,8 @@
 \begin{syntax}
-term ::= { "\lambda" binders ";" term } ; abstraction
-| { ext-quantifier "(" term "," term "," term ")" };
+term ::= "\lambda" binders ";" term ; abstraction
+| ext-quantifier "(" term "," term "," term ")" ;
 | { "{" term "\with" "[" range "]" "=" term "}" } ;
 \
-{ ext-quantifier } ::= { "\max" } | { "\min" } | { "\sum" };
-                       | { "\product" } | { "\numof" }
+ext-quantifier ::= { "\max" } | { "\min" } | "\sum" ;
+                 | "\product" | "\numof"
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index 328721a32e7a6568edcf86cbe73b61207b560940..e6b5595433569541dee778ed6abe3702a5ab5f0f 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -52,7 +52,8 @@ currently implemented into the \framac's \eacsl plug-in.
       & built-in function \lstinline|\\length| over arrays \\
       & conversions of structure to structure \\
       & t-sets \\
-      & higher-order logic constructs \\
+      & abstractions \\
+      & \lstinline|\\max| and \lstinline|\\min| \\
       & hybrid functions \\
       & labeled memory-related built-in functions \\
       & finite sets \\
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 95b64e165d07ba766576e39831fadf8695fb22a6..8adb8844f77aef4d0dc1db1e1ef4eada954624a5 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -736,7 +736,7 @@ through semantic criteria.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Higher-order logic constructions}}
+\subsection{Higher-order logic constructions}
 \label{sec:higherorder}
 
 \experimental
@@ -754,6 +754,9 @@ higher-order logic.
 \label{fig:gram:higherorder}
 \end{figure}
 
+{\highlightnotimplemented Abstractions are only implemented for extended
+  quantifiers, such as the term \lstinline|\sum(1, 10, \lambda integer k; k)|.}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{\notimplemented{Concrete logic types}}
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 71828d7d18a3c128f5a5001a20fbd8e46ed0aca5..04724d513b504014bc702496717c082f8bc61dc4 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -290,6 +290,24 @@ let cast ~src ~dst = match src, dst with
        certainly on purpose . *)
     dst
 
+(* a-b; or 0 if negative *)
+let length a b = Z.max Z.zero (Z.add Z.one (Z.sub a b))
+
+(* minimal distance between two intervals given by their respective lower and
+   upper bounds, i.e. the length between the lower bound of the second interval
+   bound and the upper bound of the first interval. *)
+let min_delta (_, max1) (min2, _) = match max1, min2 with
+  | Some m1, Some m2 -> length m2 m1
+  | _, None | None, _ -> Z.zero
+
+(* maximal distance between between two intervals given by their respective
+   lower and upper bounds, i.e. the length between the upper bound of the second
+   interval and the lower bound of the first interval.
+   @return None for \infty *)
+let max_delta (min1, _) (_, max2) = match min1, max2 with
+  | Some m1, Some m2 -> Some (length m2 m1)
+  | _, None | None, _ -> None
+
 (* ********************************************************************* *)
 (* constructors and destructors *)
 (* ********************************************************************* *)
@@ -346,49 +364,6 @@ let extended_interv_of_typ ty = match interv_of_typ ty with
   | Rational | Real | Nan | Float (_,_) as i
     -> i
 
-(* Compute the interval of the extended quantifier \sum, \product and \numof.
-   [lbd_ival] is the interval of the lambda term, [k_ival] is the interval of the
-   quantifier and [name]  is the identifier of the extended quantifier (\sum,
-   \product or \numof). The returned ival is the interval of the extended
-   quantifier *)
-let interv_of_extended_quantifier lambda i j name =
-  match lambda, i, j, name.lv_name with
-  | Ival lbd_ival, Ival i_ival, Ival j_ival, "\\sum" ->
-    (try
-       let min_lambda, max_lambda = Ival.min_and_max lbd_ival in
-       let i_inf, i_sup = Ival.min_and_max i_ival in
-       let j_inf, j_sup = Ival.min_and_max j_ival in
-       let compute_bound bound_lambda is_inf_bound =
-         let cond =
-           match bound_lambda with
-           | Some lambda ->
-             (is_inf_bound && ((Z.compare lambda Z.zero)==1)) ||
-             ((not is_inf_bound) && ((Z.compare lambda Z.zero)=(-1)))
-           | None -> false
-         in
-         match bound_lambda, i_inf, i_sup, j_inf, j_sup with
-         | Some lambda, _,Some i_sup, Some j_inf, _  when cond->
-           Some (Z.mul lambda (Z.max (Z.sub j_inf i_sup) Z.zero))
-         | _, _, _, _, _ when cond -> Some Z.zero
-         | Some lambda,  Some i_inf, _, _, Some j_sup ->
-           Some (Z.mul lambda (Z.max (Z.sub j_sup i_inf) Z.zero))
-         | Some lambda, _, _ , _, _ when (Z.compare lambda Z.zero) = 0 ->
-           Some Z.zero
-         | None, Some i_inf, _, _, Some j_sup when (Z.compare j_sup i_inf) = 0 ->
-           Some Z.zero
-         |  _, _, _, _, _ -> None
-       in
-       Ival
-         (Ival.inject_range
-            (compute_bound min_lambda true)
-            (compute_bound max_lambda false))
-     with Abstract_interp.Error_Bottom ->
-       bottom)
-  | _, _, _, "\\product" ->  Error.not_yet "product"
-  | _, _, _, "\\numof" ->  Error.not_yet "numof"
-  | _, _, _, _ -> Options.fatal  "%a is not a valid extended quantifier"
-                    Printer.pp_logic_var name
-
 let interv_of_logic_typ = function
   | Ctype ty -> interv_of_typ ty
   | Linteger -> top_ival
@@ -557,7 +532,7 @@ end = struct
 end
 
 (* ********************************************************************* *)
-(* Main algorithm *)
+(* Main functions *)
 (* ********************************************************************* *)
 
 let infer_sizeof ty =
@@ -568,6 +543,102 @@ let infer_alignof ty =
   try singleton_of_int (Cil.bytesAlignOf ty)
   with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
 
+(* Infer the interval of an extended quantifier \sum or \product.
+   [lambda] is the interval of the lambda term, [min] (resp. [max]) is the
+   interval of the minimum (resp. maximum) and [oper] is the identifier of the
+   extended quantifier (\sum, or \product). The returned ival is the interval of
+   the extended quantifier. *)
+let infer_sum_product oper lambda min max = match lambda, min, max with
+  | Ival lbd_iv, Ival lb_iv, Ival ub_iv ->
+    (try
+       let min_lambda, max_lambda = Ival.min_and_max lbd_iv in
+       let minmax_lb = Ival.min_and_max lb_iv in
+       let minmax_ub = Ival.min_and_max ub_iv in
+       let lb, ub = match oper.lv_name with
+         | "\\sum" ->
+           (* the lower (resp. upper) bound is the min (resp. max) value of the
+              lambda term, times the min (resp. max) distance between them if
+              the sign is positive, or conversely if the sign is negative *)
+           let lb = match min_lambda with
+             | None -> None
+             | Some z ->
+               if Z.sign z = -1
+               then Option.map (Z.mul z) (max_delta minmax_lb minmax_ub)
+               else Some (Z.mul z (min_delta minmax_lb minmax_ub))
+           in
+           let ub = match max_lambda with
+             | None -> None
+             | Some z ->
+               if Z.sign z = -1
+               then Some (Z.mul z (min_delta minmax_lb minmax_ub))
+               else Option.map (Z.mul z) (max_delta minmax_lb minmax_ub)
+           in
+           lb, ub
+         | "\\product" ->
+           (* the lower (resp. upper) bound is the min (resp. max) value of the
+              lambda term in absolute value, power the min (resp. max) distance
+              between them if the sign is positive, or conversely for both the
+              lambda term and the exponent if the sign is negative. If the sign
+              is negative, the minimum is also negative. *)
+           let min, max =
+             match min_lambda, max_lambda with
+             | None, None as res -> res
+             | None, Some m | Some m, None -> Some m, None
+             | Some min, Some max ->
+               let abs_min = Z.abs min in
+               let abs_max = Z.abs max in
+               Some (Z.min abs_min abs_max), Some (Z.max abs_min abs_max)
+           in
+           let lb = match min_lambda with
+             | None -> None
+             | Some z ->
+               if Z.sign z = -1 then
+                 (* the lower bound is (possibly) negative *)
+                 Extlib.opt_map2
+                   (fun m max ->
+                      match min_lambda, max_lambda with
+                      | Some mil, Some mal when Z.lt (Z.abs mil) (Z.abs mal) ->
+                        (* [lambda] contains both positive and negative values
+                           and |mil| < |mal|: instead of [-mal^m], the min is
+                           optimized to [mil * mal^(m-1)] *)
+                        Z.mul mil (Z.pow max (Z.to_int m - 1))
+                      | None, _ | _, None | Some _, Some _ ->
+                        Z.neg (Z.pow max (Z.to_int m)))
+                   (max_delta minmax_lb minmax_ub)
+                   max
+               else
+                 (* all numbers are positive:
+                    the lower bound is necessarily positive *)
+                 Option.map
+                   (fun m -> Z.pow m (Z.to_int (min_delta minmax_lb minmax_ub)))
+                   min
+           in
+           let ub =
+             Extlib.opt_map2
+               (fun m max ->
+                  match max_lambda with
+                  | 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,
+                       it is possible to reduce the number of iteration by 1. *)
+                    let exp = Z.to_int m in
+                    Z.pow max (exp - exp mod 2)
+                  | None | Some _ ->
+                    Z.pow max (Z.to_int m))
+               (max_delta minmax_lb minmax_ub)
+               max
+           in
+           lb, ub
+         | s ->
+           Options.fatal "unexpect logic function '%s'" s
+       in
+       Ival (Ival.inject_range lb ub)
+     with
+     | Abstract_interp.Error_Bottom -> bottom
+     | Z.Overflow (* if the exponent of \product is too high *) -> top_ival)
+  | _ -> Error.not_yet "extended quantifiers with non-integer parameters"
+
 let rec infer t =
   let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
   match t.term_node with
@@ -669,8 +740,7 @@ let rec infer t =
      | _ -> assert false)
   | Tnull  -> singleton_of_int 0
   | TLogic_coerce (_, t) -> infer t
-
-  | Tapp (li, _, args) ->
+  | Tapp (li, lst, args) ->
     (match li.l_body with
      | LBpred _ ->
        Ival Ival.zero_or_one
@@ -688,20 +758,50 @@ let rec infer t =
            fixpoint i
        in
        fixpoint bottom
-     | LBnone when li.l_var_info.lv_name = "\\sum" ->
+     | LBnone when li.l_var_info.lv_name = "\\sum" ||
+                   li.l_var_info.lv_name = "\\product" ->
+       (match args with
+        | [ t1; t2; { term_node = Tlambda([ k ], _) } as lambda ] ->
+          let t1_iv = infer t1 in
+          let t2_iv = infer t2 in
+          let k_iv = join t1_iv t2_iv in
+          Env.add k k_iv;
+          let lambda_iv = infer lambda in
+          Env.remove k;
+          let t2incr =
+            Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
+          in
+          (* it is correct and precise to use k_ival to compute lambda_ival, but
+             not during the code generation since the type used for k is the
+             greatest type between the type of t1 and the type of t2+1, that is
+             why the ival associated to k is updated *)
+          Env.add k (join t1_iv (infer t2incr));
+          (* k is removed during code generation, it is needed for generating
+             the code of the lambda term *)
+          infer_sum_product li.l_var_info lambda_iv t1_iv t2_iv
+        | _ -> Error.not_yet "extended quantifiers without lambda term")
+     | LBnone when li.l_var_info.lv_name = "\\numof" ->
        (match args with
-        | [ t1; t2; {term_node = Tlambda([ k ], _)} as lambda ] ->
-          let i_ival = infer t1 in
-          let j_ival = infer t2 in
-          let k_ival = join i_ival j_ival in
-          Env.add k k_ival;
-          (*k is removed during code generation, it is needed for generating the
-            code of the lambda term*)
-          let lambda_ival = infer lambda in
-          interv_of_extended_quantifier
-            lambda_ival i_ival j_ival li.l_var_info
-        | _ -> Options.fatal "unexpected input for an extended quantifier %a"
-                 Printer.pp_logic_var li.l_var_info)
+        | [ t1; t2; { term_node = Tlambda([ k ], p) } ] ->
+          let logic_info = Cil_const.make_logic_info "\\sum" in
+          logic_info.l_type <- li.l_type;
+          logic_info.l_tparams <- li.l_tparams;
+          logic_info.l_labels <- li.l_labels;
+          logic_info.l_profile <- li.l_profile;
+          logic_info.l_body <- li.l_body;
+          let numof_as_sum =
+            let conditional_term =
+              Logic_const.term
+                (Tif(p, Cil.lone (), Cil.lzero ())) Linteger
+            in
+            let lambda_term =
+              Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
+            in
+            (Logic_const.term
+               (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
+          in infer numof_as_sum
+        | _ ->
+          Options.fatal "unexpected input for an extended quantifier \\numof")
      | LBnone
      | LBreads _ ->
        (match li.l_type with
@@ -786,6 +886,6 @@ include D
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
  *)
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index 127726f6ac275c06b5ac13d26795a1a3b651b575..f1740a931076dd3e5bf4e7297a5e2a63fd70582b 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -117,6 +117,6 @@ val infer: Cil_types.term -> t
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index bf3370f975d3f58db37bd760fdc0967d6cee953c..db78316a1b6e841c86f00c68957261cd18d0b414 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -605,7 +605,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
           end
         | LBnone ->
           (match args with
-           | [ t1; t2; lambda ] ->
+           | [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ] ->
              let anonymous =
                Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
              in
@@ -623,13 +623,12 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
              ignore (type_term ~use_gmp_opt:true ?ctx ~lenv lambda);
              dup ty
            | [ ] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ ->
-             Error.not_yet "logic functions or predicates with no definition \
-                            nor reads clause"
              (* TODO : improve error message to distinguish error messages
                 corresponding to unsupported primitives and wrong application
                 of supported primitive
                 (one is a fatal and the other is a not_yet) *)
-          )
+             Error.not_yet "logic functions or predicates with no definition \
+                            nor reads clause")
         | LBreads _ ->
           Error.not_yet "logic functions or predicates performing read accesses"
         | LBinductive _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index af6d07919867996f9c7a97af3dcfcfb20810e932..5266965f380027bb921c0bc82538219872020458 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -190,110 +190,108 @@ and tlval_to_lval kf env (host, offset) =
   let name = match offset with NoOffset -> name | Field _ | Index _ -> "" in
   (host, offset), env, name
 
-(* Compute the expression which corresponds to an extended_quantifier term in a
-   given environment. [t] is the extended_quantifier term, [t_min] the lower bound,
-   [t max] the upper bound, [lambda] the lambda term and [name] is the identifier of
-   the extended quantifier ("\sum", "\product" or "\numof") *)
+(* Translate extended_quantifier terms to expressions in a given environment.
+   [t] is the extended_quantifier term, [t_min] the lower bound, [t max] the
+   upper bound, [lambda] the lambda term and [name] is the identifier of the
+   extended quantifier ("\sum" or "\product").  Do not take care of "\numof"
+   that have already been converted to "\sum". *)
 and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
-  let e, adata, env =
-    match name.lv_name,lambda.term_node with
-    | "\\sum", Tlambda([ k ] ,lt) ->
-      let ty_sum = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
-      let ty_k = match Typing.get_cast ~lenv:(Env.Local_vars.get env) t_min with
-        |Some e ->e
-        | _ -> Options.fatal "unexpected error in \\sum translation"
-      in
-      let e_min, adata, env = term_to_exp ~adata kf env t_min in
-      let e_max, adata, env = term_to_exp ~adata kf env t_max in
-      let k_as_varinfo, k_as_exp, env =
-        Env.Logic_binding.add ~ty:ty_k env kf k
-      in
-      let init_k_stmt =
-        Gmp.init_set ~loc (Cil.var k_as_varinfo) k_as_exp e_min
-      in
-      (*variable initialization*)
-      (*one = 1;*)
-      let _, one_as_exp, env =
-        create_and_init_var ~loc kf ty_k "one" (Cil.one ~loc) env
-      in
-      (*cond = 0;*)
-      let cond_as_varinfo, cond_as_exp, env =
-        create_and_init_var ~loc kf Cil.intType "cond" (Cil.zero ~loc) env
-      in
-      (*lbda = 0;*)
-      let lbd_as_varinfo, lbd_as_exp, env =
-        create_and_init_var ~loc kf ty_sum "lambda" (Cil.zero ~loc) env
-      in
-      (*sum = 0;*)
-      let sum_as_varinfo, sum_as_exp, env =
-        create_and_init_var ~loc kf ty_sum "sum" (Cil.zero ~loc) env
-      in
-      (*lambda_as_varinfo  affectation*)
-      let env = Env.push env in
-      let e_lbd, _, env = term_to_exp ~adata:Assert.no_data kf env lt in
-      Interval.Env.remove k;
-      let lbd_stmt,env =
-        Env.pop_and_get env
-          (Gmp.affect ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
-          false Env.Middle
-      in
-      (*statement construction*)
-      (*cond = k > e_max; or cond =  __gmpz_cmp(k,e_max)*)
-      let cond_stmt =
-        affect_binop ~loc cond_as_varinfo None Gt ty_k k_as_exp e_max
-      in
-      (*sum = sum + lbda; or __gmpz_add(sum,sum,lbda);*)
-      let sum_plus_lbd_stmt =
-        affect_binop
-          ~loc
-          sum_as_varinfo
-          (Some sum_as_exp)
-          PlusA
-          ty_sum
-          sum_as_exp
-          lbd_as_exp
-      in
-      (*k = k + one; or __gmpz_add(k,k,one);*)
-      let k_plus_one_stmt =
-        affect_binop
-          ~loc k_as_varinfo (Some k_as_exp) PlusA ty_k k_as_exp one_as_exp
-      in
-      (*if ty_k is gmpz then the result of the comparison must be interpreted
-        as true if cond=1 and as false if cond=0 or -1 because of the semantics
-        of __gmpz_cmp. That differs from the conventional interpretation*)
-      let cond_as_exp =
-        if Gmp_types.Z.is_t ty_k then
-          (Cil.mkBinOp ~loc Gt cond_as_exp (Cil.zero ~loc))
-        else
-          cond_as_exp
-      in
-      (*statement combination*)
-      let if_stmt =
-        Smart_stmt.if_stmt
-          ~loc
-          ~cond:cond_as_exp
-          ~else_blk:
-            (Cil.mkBlock [
-                Smart_stmt.block_stmt lbd_stmt;
-                sum_plus_lbd_stmt;
-                k_plus_one_stmt
-              ])
-          (Cil.mkBlock [ Smart_stmt.break ~loc ])
-      in
-      let for_stmt =
-        Smart_stmt.stmt
-          (Loop([],Cil.mkBlock [ cond_stmt; if_stmt ],loc,None,None))
-      in
-      let final_stmt  = (Cil.mkBlock [ init_k_stmt; for_stmt ]) in
-      Env.Logic_binding.remove env k;
-      let env = Env.add_stmt env kf (Smart_stmt.block_stmt final_stmt) in
-      sum_as_exp, adata, env
-    | "\\product", _ | "\\numof", _ -> Error.not_yet "\\product and \\numof"
-    | _, _ -> Options.fatal  "%a is not a valid extended quantifier"
-                Printer.pp_logic_var name
-  in
-  let adata, env = Assert.register_term ~loc kf env t e adata in
-  e, adata, env, Typed_number.C_number, ""
+  match lambda.term_node with
+  | Tlambda([ k ] ,lt)
+    when name.lv_name = "\\product" || name.lv_name = "\\sum"
+    ->
+    let ty_op = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty_k = match Typing.get_cast ~lenv:(Env.Local_vars.get env) t_min with
+      | Some e -> e
+      | _ -> Options.fatal "unexpected error in \\sum translation"
+    in
+    let e_min, adata, env = term_to_exp ~adata kf env t_min in
+    let e_max, adata, env = term_to_exp ~adata kf env t_max in
+    let k_as_varinfo, k_as_exp, env = Env.Logic_binding.add ~ty:ty_k env kf k in
+    let init_k_stmt = Gmp.init_set ~loc (Cil.var k_as_varinfo) k_as_exp e_min in
+    (* variable initialization *)
+    (* one = 1; *)
+    let _, one_as_exp, env =
+      create_and_init_var ~loc kf ty_k "one" (Cil.one ~loc) env
+    in
+    (* cond = 0; *)
+    let cond_as_varinfo, cond_as_exp, env =
+      create_and_init_var ~loc kf Cil.intType "cond" (Cil.zero ~loc) env
+    in
+    (* lbda = 0; *)
+    let lbd_as_varinfo, lbd_as_exp, env =
+      create_and_init_var ~loc kf ty_op "lambda" (Cil.zero ~loc) env
+    in
+    (* accumulator = neutral value; *)
+    let acc_as_varinfo, acc_as_exp, env = if name.lv_name="\\sum" then
+        create_and_init_var ~loc kf ty_op "accumulator" (Cil.zero ~loc) env
+      else
+        create_and_init_var ~loc kf ty_op "accumulator" (Cil.one ~loc) env
+    in
+    (* lambda_as_varinfo assignment *)
+    let env = Env.push env in
+    let e_lbd, _, env = term_to_exp ~adata:Assert.no_data kf env lt in
+    Interval.Env.remove k;
+    let lbd_stmt,env =
+      Env.pop_and_get env
+        (Gmp.affect ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
+        false Env.Middle
+    in
+    (* statement construction *)
+    (* cond = k > e_max; or cond =  __gmpz_cmp(k,e_max) *)
+    let cond_stmt =
+      affect_binop ~loc cond_as_varinfo None Gt ty_k k_as_exp e_max
+    in
+    (* acc = acc op lbda; or __gmpz_op(acc,acc,lbda); *)
+    let op = if name.lv_name = "\\sum" then PlusA else Mult in
+    let acc_plus_lbd_stmt =
+      affect_binop
+        ~loc
+        acc_as_varinfo
+        (Some acc_as_exp)
+        op
+        ty_op
+        acc_as_exp
+        lbd_as_exp
+    in
+    (* k = k + one; or __gmpz_add(k,k,one); *)
+    let k_plus_one_stmt =
+      affect_binop
+        ~loc k_as_varinfo (Some k_as_exp) PlusA ty_k k_as_exp one_as_exp
+    in
+    (* if [ty_k] is gmpz, then the result of the comparison must be interpreted
+       as [true] if [cond == 1] and as [false] if [cond == 0] or [-1] because of
+       the semantics of __gmpz_cmp. That differs from the conventional
+       interpretation. *)
+    let cond_as_exp =
+      if Gmp_types.Z.is_t ty_k then
+        (Cil.mkBinOp ~loc Gt cond_as_exp (Cil.zero ~loc))
+      else
+        cond_as_exp
+    in
+    (* statement combination *)
+    let if_stmt =
+      Smart_stmt.if_stmt
+        ~loc
+        ~cond:cond_as_exp
+        ~else_blk:
+          (Cil.mkBlock
+             [ Smart_stmt.block_stmt lbd_stmt;
+               acc_plus_lbd_stmt;
+               k_plus_one_stmt ])
+        (Cil.mkBlock [ Smart_stmt.break ~loc ])
+    in
+    let for_stmt =
+      Smart_stmt.stmt
+        (Loop([],Cil.mkBlock [ cond_stmt; if_stmt ],loc,None,None))
+    in
+    let final_stmt  = (Cil.mkBlock [ init_k_stmt; for_stmt ]) in
+    Env.Logic_binding.remove env k;
+    let env = Env.add_stmt env kf (Smart_stmt.block_stmt final_stmt) in
+    let adata, env = Assert.register_term ~loc kf env t acc_as_exp adata in
+    acc_as_exp, adata, env, Typed_number.C_number, ""
+  | _ ->
+    assert false
 
 and context_insensitive_term_to_exp ~adata kf env t =
   let loc = t.term_loc in
@@ -742,12 +740,37 @@ and context_insensitive_term_to_exp ~adata kf env t =
     let e = Cil.mkAddrOrStartOf ~loc lv in
     let adata, env = Assert.register_term ~loc kf env t e adata in
     e, adata, env, Typed_number.C_number, "startof"
-  | Tapp(li, _, [ t1; t2; lambda ]) when li.l_body = LBnone ->
+  | Tapp(li, _, [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ])
+    when li.l_body = LBnone && (li.l_var_info.lv_name = "\\sum" ||
+                                li.l_var_info.lv_name = "\\product")->
     extended_quantifier_to_exp ~adata ~loc kf env t t1 t2 lambda li.l_var_info
-  | Tapp(_, _, _) ->
+  | Tapp(li, lst, [ t1; t2; {term_node = Tlambda([ k ], predicate)}])
+    when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
+    let logic_info = Cil_const.make_logic_info "\\sum" in
+    logic_info.l_type <- li.l_type;
+    logic_info.l_tparams <- li.l_tparams;
+    logic_info.l_labels <- li.l_labels;
+    logic_info.l_profile <- li.l_profile;
+    logic_info.l_body <- li.l_body;
+    let numof_as_sum =
+      let conditional_term =
+        Logic_const.term
+          (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
+      in
+      let lambda_term =
+        Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
+      in
+      (Logic_const.term
+         (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
+    in
+    Typing.type_term ~use_gmp_opt:true numof_as_sum;
+    context_insensitive_term_to_exp ~adata kf env numof_as_sum
+  | Tapp(_, [], _) ->
     let e, adata, env = Logic_functions.tapp_to_exp ~adata kf env t in
     let adata, env = Assert.register_term ~loc kf env t e adata in
     e, adata, env, Typed_number.C_number, "app"
+  | Tapp(_, _ :: _, _) ->
+    Env.not_yet env "logic functions or predicates with labels"
   | Tlambda(_, lt) ->
     let exp, adata, env = term_to_exp ~adata kf env lt in
     exp, adata, env, Typed_number.C_number, ""
diff --git a/src/plugins/e-acsl/tests/arith/extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/extended_quantifiers.c
new file mode 100644
index 0000000000000000000000000000000000000000..a3abd3674abba6e1762f2018448959e837ec60c7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/extended_quantifiers.c
@@ -0,0 +1,33 @@
+/* run.config
+   COMMENT: sum operations
+*/
+
+#include <limits.h>
+
+int main(void) {
+  unsigned long x = UINT_MAX;
+  int y = 10;
+
+  /*@ assert \sum(2, 10, \lambda integer k; 2 * k) == 108; */;
+  /*@ assert \sum(2, 35, \lambda integer k; ULLONG_MAX) != 0; */;
+  /*@ assert \sum(10, 2, \lambda integer k; k) == 0; */;
+  /*@ assert \sum(x * x, 2, \lambda integer k; k) == 0; */;
+  /*@ assert \sum(ULLONG_MAX - 5, ULLONG_MAX, \lambda integer k; 1) == 6; */;
+  /*@ assert \sum(INT_MAX, INT_MAX, \lambda integer k; k) + 1 > INT_MAX; */
+  /*@ assert \let x = (0 == 0) ? 1 : 10;
+    @        \sum (x, 10, \lambda integer k; INT_MIN) < 0; */
+
+  /*@ assert \numof(2, 10, \lambda integer k; k - 2 >= 0) == 9; */;
+  /*@ assert \numof(UINT_MAX - 5, UINT_MAX, \lambda integer k; k % 2 == 1)
+    @        == 3; */
+  ;
+
+  /*@ assert \product(1, 100, \lambda integer k; k) >= 3628800; */;
+  /*@ assert \product(1, 10, \lambda integer k; k) == 3628800; */;
+  /*@ assert \product(-10, 10, \lambda integer k; k) == 0; */;
+  /*@ assert \product(-20, -1, \lambda integer k; 2 * k)
+    @     == \product(1, 20, \lambda integer k; 2 * k); */
+  ;
+
+  return 0;
+}
diff --git a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3fcbe6979c0408e461a31fcabe4acf5d8d0a67f8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
@@ -0,0 +1,97 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/extended_quantifiers.c:11: Warning: 
+  signed overflow. assert 2 * __gen_e_acsl_k ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:11: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_accumulator + __gen_e_acsl_lambda ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:11: Warning: 
+  signed overflow. assert __gen_e_acsl_k + __gen_e_acsl_one ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:11: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:11: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:12: Warning: 
+  signed overflow. assert __gen_e_acsl_k_2 + __gen_e_acsl_one_2 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:12: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:12: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:13: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:14: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:14: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:15: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_accumulator_5 + __gen_e_acsl_lambda_5 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:15: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:15: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:16: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:16: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:18: Warning: 
+  signed overflow.
+  assert
+  -9223372036854775808 ≤ __gen_e_acsl_accumulator_7 + __gen_e_acsl_lambda_7;
+[eva:alarm] tests/arith/extended_quantifiers.c:18: Warning: 
+  signed overflow. assert __gen_e_acsl_k_7 + __gen_e_acsl_one_7 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:17: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:17: Warning: 
+  assertion got status unknown.
+[eva:alarm] :0: Warning: 
+  signed overflow. assert __gen_e_acsl_k_8 + __gen_e_acsl_one_8 ≤ 2147483647;
+[eva:alarm] :0: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_accumulator_8 + __gen_e_acsl_lambda_8 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:20: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:20: Warning: 
+  assertion got status unknown.
+[eva:alarm] :0: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_accumulator_9 + __gen_e_acsl_lambda_9 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:21: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:21: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:25: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_k_10 + __gen_e_acsl_one_10 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:25: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:25: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+  signed overflow. assert 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_k_15 + __gen_e_acsl_one_13 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning: 
+  signed overflow. assert 2 * __gen_e_acsl_k_16 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning: 
+  signed overflow.
+  assert __gen_e_acsl_k_16 + __gen_e_acsl_one_14 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+  assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
new file mode 100644
index 0000000000000000000000000000000000000000..0dc365800f3a322f927c8f285959f3d817a014eb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -0,0 +1,571 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+int main(void)
+{
+  int __retres;
+  unsigned long x = (unsigned long)4294967295U;
+  int y = 10;
+  {
+    int __gen_e_acsl_k;
+    int __gen_e_acsl_one;
+    int __gen_e_acsl_cond;
+    int __gen_e_acsl_lambda;
+    int __gen_e_acsl_accumulator;
+    __gen_e_acsl_one = 1;
+    __gen_e_acsl_cond = 0;
+    __gen_e_acsl_lambda = 0;
+    __gen_e_acsl_accumulator = 0;
+    __gen_e_acsl_k = 2;
+    while (1) {
+      __gen_e_acsl_cond = __gen_e_acsl_k > 10;
+      if (__gen_e_acsl_cond) break;
+      else {
+        /*@ assert Eva: signed_overflow: 2 * __gen_e_acsl_k ≤ 2147483647;
+        */
+        __gen_e_acsl_lambda = 2 * __gen_e_acsl_k;
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_accumulator + __gen_e_acsl_lambda ≤ 2147483647;
+        */
+        __gen_e_acsl_accumulator += __gen_e_acsl_lambda;
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k + __gen_e_acsl_one ≤ 2147483647;
+        */
+        __gen_e_acsl_k += __gen_e_acsl_one;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator == 108,1,"Assertion","main",
+                    "\\sum(2, 10, \\lambda integer k; 2 * k) == 108",
+                    "tests/arith/extended_quantifiers.c",11);
+  }
+  /*@ assert \sum(2, 10, \lambda ℤ k; 2 * k) ≡ 108; */ ;
+  {
+    int __gen_e_acsl_k_2;
+    int __gen_e_acsl_one_2;
+    int __gen_e_acsl_cond_2;
+    __e_acsl_mpz_t __gen_e_acsl_lambda_2;
+    __e_acsl_mpz_t __gen_e_acsl_accumulator_2;
+    __e_acsl_mpz_t __gen_e_acsl__2;
+    int __gen_e_acsl_ne;
+    __gen_e_acsl_one_2 = 1;
+    __gen_e_acsl_cond_2 = 0;
+    __gmpz_init_set_si(__gen_e_acsl_lambda_2,0L);
+    __gmpz_init_set_si(__gen_e_acsl_accumulator_2,0L);
+    __gen_e_acsl_k_2 = 2;
+    while (1) {
+      __gen_e_acsl_cond_2 = __gen_e_acsl_k_2 > 35;
+      if (__gen_e_acsl_cond_2) break;
+      else {
+        {
+          __e_acsl_mpz_t __gen_e_acsl_;
+          __gmpz_init_set_ui(__gen_e_acsl_,18446744073709551615UL);
+          __gmpz_set(__gen_e_acsl_lambda_2,
+                     (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+          __gmpz_clear(__gen_e_acsl_);
+        }
+        __gmpz_add(__gen_e_acsl_accumulator_2,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_2),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_2));
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_2 + __gen_e_acsl_one_2 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_2 += __gen_e_acsl_one_2;
+      }
+    }
+    __gmpz_init_set_si(__gen_e_acsl__2,0L);
+    __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_2),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+    __e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","main",
+                    "\\sum(2, 35, \\lambda integer k; 18446744073709551615ULL) != 0",
+                    "tests/arith/extended_quantifiers.c",12);
+    __gmpz_clear(__gen_e_acsl_lambda_2);
+    __gmpz_clear(__gen_e_acsl_accumulator_2);
+    __gmpz_clear(__gen_e_acsl__2);
+  }
+  /*@ assert \sum(2, 35, \lambda ℤ k; 18446744073709551615ULL) ≢ 0; */ ;
+  {
+    int __gen_e_acsl_k_3;
+    int __gen_e_acsl_one_3;
+    int __gen_e_acsl_cond_3;
+    int __gen_e_acsl_lambda_3;
+    int __gen_e_acsl_accumulator_3;
+    __gen_e_acsl_one_3 = 1;
+    __gen_e_acsl_cond_3 = 0;
+    __gen_e_acsl_lambda_3 = 0;
+    __gen_e_acsl_accumulator_3 = 0;
+    __gen_e_acsl_k_3 = 10;
+    while (1) {
+      __gen_e_acsl_cond_3 = __gen_e_acsl_k_3 > 2;
+      if (__gen_e_acsl_cond_3) break;
+      else {
+        __gen_e_acsl_lambda_3 = __gen_e_acsl_k_3;
+        __gen_e_acsl_accumulator_3 += __gen_e_acsl_lambda_3;
+        __gen_e_acsl_k_3 += __gen_e_acsl_one_3;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_3 == 0,1,"Assertion","main",
+                    "\\sum(10, 2, \\lambda integer k; k) == 0",
+                    "tests/arith/extended_quantifiers.c",13);
+  }
+  /*@ assert \sum(10, 2, \lambda ℤ k; k) ≡ 0; */ ;
+  {
+    __e_acsl_mpz_t __gen_e_acsl_x;
+    __e_acsl_mpz_t __gen_e_acsl_mul;
+    __e_acsl_mpz_t __gen_e_acsl__3;
+    __e_acsl_mpz_t __gen_e_acsl_k_4;
+    __e_acsl_mpz_t __gen_e_acsl_one_4;
+    int __gen_e_acsl_cond_4;
+    __e_acsl_mpz_t __gen_e_acsl_lambda_4;
+    __e_acsl_mpz_t __gen_e_acsl_accumulator_4;
+    __e_acsl_mpz_t __gen_e_acsl__4;
+    int __gen_e_acsl_eq;
+    __gmpz_init_set_ui(__gen_e_acsl_x,x);
+    __gmpz_init(__gen_e_acsl_mul);
+    __gmpz_mul(__gen_e_acsl_mul,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
+    __gmpz_init_set_si(__gen_e_acsl__3,2L);
+    __gmpz_init_set_si(__gen_e_acsl_one_4,1L);
+    __gen_e_acsl_cond_4 = 0;
+    __gmpz_init_set_si(__gen_e_acsl_lambda_4,0L);
+    __gmpz_init_set_si(__gen_e_acsl_accumulator_4,0L);
+    __gmpz_init_set(__gen_e_acsl_k_4,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+    while (1) {
+      __gen_e_acsl_cond_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
+                                       (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+      if (__gen_e_acsl_cond_4 > 0) break;
+      else {
+        __gmpz_set(__gen_e_acsl_lambda_4,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4));
+        __gmpz_add(__gen_e_acsl_accumulator_4,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_4),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_4));
+        __gmpz_add(__gen_e_acsl_k_4,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_4));
+      }
+    }
+    __gmpz_init_set_si(__gen_e_acsl__4,0L);
+    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_4),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+    __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main",
+                    "\\sum(x * x, 2, \\lambda integer k; k) == 0",
+                    "tests/arith/extended_quantifiers.c",14);
+    __gmpz_clear(__gen_e_acsl_x);
+    __gmpz_clear(__gen_e_acsl_mul);
+    __gmpz_clear(__gen_e_acsl__3);
+    __gmpz_clear(__gen_e_acsl_k_4);
+    __gmpz_clear(__gen_e_acsl_one_4);
+    __gmpz_clear(__gen_e_acsl_lambda_4);
+    __gmpz_clear(__gen_e_acsl_accumulator_4);
+    __gmpz_clear(__gen_e_acsl__4);
+  }
+  /*@ assert \sum(x * x, 2, \lambda ℤ k; k) ≡ 0; */ ;
+  {
+    __e_acsl_mpz_t __gen_e_acsl__5;
+    __e_acsl_mpz_t __gen_e_acsl__6;
+    __e_acsl_mpz_t __gen_e_acsl_k_5;
+    __e_acsl_mpz_t __gen_e_acsl_one_5;
+    int __gen_e_acsl_cond_5;
+    int __gen_e_acsl_lambda_5;
+    int __gen_e_acsl_accumulator_5;
+    __gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL - 5UL);
+    __gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL);
+    __gmpz_init_set_si(__gen_e_acsl_one_5,1L);
+    __gen_e_acsl_cond_5 = 0;
+    __gen_e_acsl_lambda_5 = 0;
+    __gen_e_acsl_accumulator_5 = 0;
+    __gmpz_init_set(__gen_e_acsl_k_5,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+    while (1) {
+      __gen_e_acsl_cond_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
+                                       (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+      if (__gen_e_acsl_cond_5 > 0) break;
+      else {
+        __gen_e_acsl_lambda_5 = 1;
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_accumulator_5 + __gen_e_acsl_lambda_5 ≤
+              2147483647;
+        */
+        __gen_e_acsl_accumulator_5 += __gen_e_acsl_lambda_5;
+        __gmpz_add(__gen_e_acsl_k_5,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_5));
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_5 == 6,1,"Assertion","main",
+                    "\\sum(18446744073709551615ULL - 5, 18446744073709551615ULL,\n    \\lambda integer k; 1)\n== 6",
+                    "tests/arith/extended_quantifiers.c",15);
+    __gmpz_clear(__gen_e_acsl__5);
+    __gmpz_clear(__gen_e_acsl__6);
+    __gmpz_clear(__gen_e_acsl_k_5);
+    __gmpz_clear(__gen_e_acsl_one_5);
+  }
+  /*@
+  assert
+  \sum(18446744073709551615ULL - 5, 18446744073709551615ULL,
+      \lambda ℤ k; 1)
+  ≡ 6; */
+  ;
+  {
+    unsigned int __gen_e_acsl_k_6;
+    unsigned int __gen_e_acsl_one_6;
+    int __gen_e_acsl_cond_6;
+    unsigned int __gen_e_acsl_lambda_6;
+    unsigned int __gen_e_acsl_accumulator_6;
+    __gen_e_acsl_one_6 = 1;
+    __gen_e_acsl_cond_6 = 0;
+    __gen_e_acsl_lambda_6 = 0;
+    __gen_e_acsl_accumulator_6 = 0;
+    __gen_e_acsl_k_6 = 2147483647U;
+    while (1) {
+      __gen_e_acsl_cond_6 = __gen_e_acsl_k_6 > 2147483647U;
+      if (__gen_e_acsl_cond_6) break;
+      else {
+        __gen_e_acsl_lambda_6 = __gen_e_acsl_k_6;
+        __gen_e_acsl_accumulator_6 += __gen_e_acsl_lambda_6;
+        __gen_e_acsl_k_6 += __gen_e_acsl_one_6;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_6 + 1U > 2147483647U,1,
+                    "Assertion","main",
+                    "\\sum(2147483647, 2147483647, \\lambda integer k; k) + 1 > 2147483647",
+                    "tests/arith/extended_quantifiers.c",16);
+  }
+  /*@ assert \sum(2147483647, 2147483647, \lambda ℤ k; k) + 1 > 2147483647;
+   */
+  ;
+  {
+    int __gen_e_acsl_x_2;
+    int __gen_e_acsl_k_7;
+    int __gen_e_acsl_one_7;
+    int __gen_e_acsl_cond_7;
+    long __gen_e_acsl_lambda_7;
+    long __gen_e_acsl_accumulator_7;
+    __gen_e_acsl_x_2 = 1;
+    __gen_e_acsl_one_7 = 1;
+    __gen_e_acsl_cond_7 = 0;
+    __gen_e_acsl_lambda_7 = 0;
+    __gen_e_acsl_accumulator_7 = 0;
+    __gen_e_acsl_k_7 = __gen_e_acsl_x_2;
+    while (1) {
+      __gen_e_acsl_cond_7 = __gen_e_acsl_k_7 > 10;
+      if (__gen_e_acsl_cond_7) break;
+      else {
+        __gen_e_acsl_lambda_7 = -2147483647 - 1;
+        /*@ assert
+            Eva: signed_overflow:
+              -9223372036854775808 ≤
+              __gen_e_acsl_accumulator_7 + __gen_e_acsl_lambda_7;
+        */
+        __gen_e_acsl_accumulator_7 += __gen_e_acsl_lambda_7;
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_7 + __gen_e_acsl_one_7 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_7 += __gen_e_acsl_one_7;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_7 < 0L,1,"Assertion","main",
+                    "\\let x = 0 == 0? 1: 10; \\sum(x, 10, \\lambda integer k; -2147483647 - 1) < 0",
+                    "tests/arith/extended_quantifiers.c",17);
+  }
+  /*@
+  assert
+  \let x = 0 ≡ 0? 1: 10; \sum(x, 10, \lambda ℤ k; -2147483647 - 1) < 0;
+   */
+  ;
+  {
+    int __gen_e_acsl_k_8;
+    int __gen_e_acsl_one_8;
+    int __gen_e_acsl_cond_8;
+    int __gen_e_acsl_lambda_8;
+    int __gen_e_acsl_accumulator_8;
+    __gen_e_acsl_one_8 = 1;
+    __gen_e_acsl_cond_8 = 0;
+    __gen_e_acsl_lambda_8 = 0;
+    __gen_e_acsl_accumulator_8 = 0;
+    __gen_e_acsl_k_8 = 2;
+    while (1) {
+      __gen_e_acsl_cond_8 = __gen_e_acsl_k_8 > 10;
+      if (__gen_e_acsl_cond_8) break;
+      else {
+        {
+          int __gen_e_acsl_if;
+          if (__gen_e_acsl_k_8 - 2 >= 0) __gen_e_acsl_if = 1;
+          else __gen_e_acsl_if = 0;
+          __gen_e_acsl_lambda_8 = __gen_e_acsl_if;
+        }
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_accumulator_8 + __gen_e_acsl_lambda_8 ≤
+              2147483647;
+        */
+        __gen_e_acsl_accumulator_8 += __gen_e_acsl_lambda_8;
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_8 + __gen_e_acsl_one_8 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_8 += __gen_e_acsl_one_8;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_8 == 9,1,"Assertion","main",
+                    "\\numof(2, 10, \\lambda integer k; k - 2 >= 0) == 9",
+                    "tests/arith/extended_quantifiers.c",20);
+  }
+  /*@ assert \numof(2, 10, \lambda ℤ k; k - 2 ≥ 0) ≡ 9; */ ;
+  {
+    unsigned long __gen_e_acsl_k_9;
+    unsigned long __gen_e_acsl_one_9;
+    int __gen_e_acsl_cond_9;
+    int __gen_e_acsl_lambda_9;
+    int __gen_e_acsl_accumulator_9;
+    __gen_e_acsl_one_9 = 1;
+    __gen_e_acsl_cond_9 = 0;
+    __gen_e_acsl_lambda_9 = 0;
+    __gen_e_acsl_accumulator_9 = 0;
+    __gen_e_acsl_k_9 = 4294967295U - 5U;
+    while (1) {
+      __gen_e_acsl_cond_9 = __gen_e_acsl_k_9 > 4294967295UL;
+      if (__gen_e_acsl_cond_9) break;
+      else {
+        {
+          int __gen_e_acsl_if_2;
+          if ((int)(__gen_e_acsl_k_9 % 2UL) == 1) __gen_e_acsl_if_2 = 1;
+          else __gen_e_acsl_if_2 = 0;
+          __gen_e_acsl_lambda_9 = __gen_e_acsl_if_2;
+        }
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_accumulator_9 + __gen_e_acsl_lambda_9 ≤
+              2147483647;
+        */
+        __gen_e_acsl_accumulator_9 += __gen_e_acsl_lambda_9;
+        __gen_e_acsl_k_9 += __gen_e_acsl_one_9;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_9 == 3,1,"Assertion","main",
+                    "\\numof(4294967295U - 5, 4294967295U, \\lambda integer k; k % 2 == 1) == 3",
+                    "tests/arith/extended_quantifiers.c",21);
+  }
+  /*@
+  assert
+  \numof(4294967295U - 5, 4294967295U, \lambda ℤ k; k % 2 ≡ 1) ≡ 3; */
+  ;
+  {
+    int __gen_e_acsl_k_10;
+    int __gen_e_acsl_one_10;
+    int __gen_e_acsl_cond_10;
+    __e_acsl_mpz_t __gen_e_acsl_lambda_10;
+    __e_acsl_mpz_t __gen_e_acsl_accumulator_10;
+    __e_acsl_mpz_t __gen_e_acsl__7;
+    int __gen_e_acsl_ge;
+    __gen_e_acsl_one_10 = 1;
+    __gen_e_acsl_cond_10 = 0;
+    __gmpz_init_set_si(__gen_e_acsl_lambda_10,0L);
+    __gmpz_init_set_si(__gen_e_acsl_accumulator_10,1L);
+    __gen_e_acsl_k_10 = 1;
+    while (1) {
+      __gen_e_acsl_cond_10 = __gen_e_acsl_k_10 > 100;
+      if (__gen_e_acsl_cond_10) break;
+      else {
+        {
+          __e_acsl_mpz_t __gen_e_acsl_k_11;
+          __gmpz_init_set_si(__gen_e_acsl_k_11,(long)__gen_e_acsl_k_10);
+          __gmpz_set(__gen_e_acsl_lambda_10,
+                     (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_11));
+          __gmpz_clear(__gen_e_acsl_k_11);
+        }
+        __gmpz_mul(__gen_e_acsl_accumulator_10,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_10),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_10));
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_10 + __gen_e_acsl_one_10 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_10 += __gen_e_acsl_one_10;
+      }
+    }
+    __gmpz_init_set_ui(__gen_e_acsl__7,3628800UL);
+    __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_10),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+    __e_acsl_assert(__gen_e_acsl_ge >= 0,1,"Assertion","main",
+                    "\\product(1, 100, \\lambda integer k; k) >= 3628800",
+                    "tests/arith/extended_quantifiers.c",25);
+    __gmpz_clear(__gen_e_acsl_lambda_10);
+    __gmpz_clear(__gen_e_acsl_accumulator_10);
+    __gmpz_clear(__gen_e_acsl__7);
+  }
+  /*@ assert \product(1, 100, \lambda ℤ k; k) ≥ 3628800; */ ;
+  {
+    int __gen_e_acsl_k_12;
+    int __gen_e_acsl_one_11;
+    int __gen_e_acsl_cond_11;
+    unsigned long __gen_e_acsl_lambda_11;
+    unsigned long __gen_e_acsl_accumulator_11;
+    __gen_e_acsl_one_11 = 1;
+    __gen_e_acsl_cond_11 = 0;
+    __gen_e_acsl_lambda_11 = 0;
+    __gen_e_acsl_accumulator_11 = 1;
+    __gen_e_acsl_k_12 = 1;
+    while (1) {
+      __gen_e_acsl_cond_11 = __gen_e_acsl_k_12 > 10;
+      if (__gen_e_acsl_cond_11) break;
+      else {
+        __gen_e_acsl_lambda_11 = (unsigned long)__gen_e_acsl_k_12;
+        __gen_e_acsl_accumulator_11 *= __gen_e_acsl_lambda_11;
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_12 += __gen_e_acsl_one_11;
+      }
+    }
+    __e_acsl_assert(__gen_e_acsl_accumulator_11 == 3628800UL,1,"Assertion",
+                    "main",
+                    "\\product(1, 10, \\lambda integer k; k) == 3628800",
+                    "tests/arith/extended_quantifiers.c",26);
+  }
+  /*@ assert \product(1, 10, \lambda ℤ k; k) ≡ 3628800; */ ;
+  {
+    int __gen_e_acsl_k_13;
+    int __gen_e_acsl_one_12;
+    int __gen_e_acsl_cond_12;
+    __e_acsl_mpz_t __gen_e_acsl_lambda_12;
+    __e_acsl_mpz_t __gen_e_acsl_accumulator_12;
+    __e_acsl_mpz_t __gen_e_acsl__8;
+    int __gen_e_acsl_eq_2;
+    __gen_e_acsl_one_12 = 1;
+    __gen_e_acsl_cond_12 = 0;
+    __gmpz_init_set_si(__gen_e_acsl_lambda_12,0L);
+    __gmpz_init_set_si(__gen_e_acsl_accumulator_12,1L);
+    __gen_e_acsl_k_13 = -10;
+    while (1) {
+      __gen_e_acsl_cond_12 = __gen_e_acsl_k_13 > 10;
+      if (__gen_e_acsl_cond_12) break;
+      else {
+        {
+          __e_acsl_mpz_t __gen_e_acsl_k_14;
+          __gmpz_init_set_si(__gen_e_acsl_k_14,(long)__gen_e_acsl_k_13);
+          __gmpz_set(__gen_e_acsl_lambda_12,
+                     (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_14));
+          __gmpz_clear(__gen_e_acsl_k_14);
+        }
+        __gmpz_mul(__gen_e_acsl_accumulator_12,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_12),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_12));
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_13 += __gen_e_acsl_one_12;
+      }
+    }
+    __gmpz_init_set_si(__gen_e_acsl__8,0L);
+    __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_12),
+                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+    __e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","main",
+                    "\\product(-10, 10, \\lambda integer k; k) == 0",
+                    "tests/arith/extended_quantifiers.c",27);
+    __gmpz_clear(__gen_e_acsl_lambda_12);
+    __gmpz_clear(__gen_e_acsl_accumulator_12);
+    __gmpz_clear(__gen_e_acsl__8);
+  }
+  /*@ assert \product(-10, 10, \lambda ℤ k; k) ≡ 0; */ ;
+  {
+    int __gen_e_acsl_k_15;
+    int __gen_e_acsl_one_13;
+    int __gen_e_acsl_cond_13;
+    __e_acsl_mpz_t __gen_e_acsl_lambda_13;
+    __e_acsl_mpz_t __gen_e_acsl_accumulator_13;
+    int __gen_e_acsl_k_16;
+    int __gen_e_acsl_one_14;
+    int __gen_e_acsl_cond_14;
+    __e_acsl_mpz_t __gen_e_acsl_lambda_14;
+    __e_acsl_mpz_t __gen_e_acsl_accumulator_14;
+    int __gen_e_acsl_eq_3;
+    __gen_e_acsl_one_13 = 1;
+    __gen_e_acsl_cond_13 = 0;
+    __gmpz_init_set_si(__gen_e_acsl_lambda_13,0L);
+    __gmpz_init_set_si(__gen_e_acsl_accumulator_13,1L);
+    __gen_e_acsl_k_15 = -20;
+    while (1) {
+      __gen_e_acsl_cond_13 = __gen_e_acsl_k_15 > -1;
+      if (__gen_e_acsl_cond_13) break;
+      else {
+        {
+          __e_acsl_mpz_t __gen_e_acsl__9;
+          /*@ assert
+              Eva: signed_overflow: 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+          */
+          __gmpz_init_set_si(__gen_e_acsl__9,(long)(2 * __gen_e_acsl_k_15));
+          __gmpz_set(__gen_e_acsl_lambda_13,
+                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+          __gmpz_clear(__gen_e_acsl__9);
+        }
+        __gmpz_mul(__gen_e_acsl_accumulator_13,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_13),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_13));
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_15 + __gen_e_acsl_one_13 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_15 += __gen_e_acsl_one_13;
+      }
+    }
+    __gen_e_acsl_one_14 = 1;
+    __gen_e_acsl_cond_14 = 0;
+    __gmpz_init_set_si(__gen_e_acsl_lambda_14,0L);
+    __gmpz_init_set_si(__gen_e_acsl_accumulator_14,1L);
+    __gen_e_acsl_k_16 = 1;
+    while (1) {
+      __gen_e_acsl_cond_14 = __gen_e_acsl_k_16 > 20;
+      if (__gen_e_acsl_cond_14) break;
+      else {
+        {
+          __e_acsl_mpz_t __gen_e_acsl__10;
+          /*@ assert
+              Eva: signed_overflow: 2 * __gen_e_acsl_k_16 ≤ 2147483647;
+          */
+          __gmpz_init_set_si(__gen_e_acsl__10,(long)(2 * __gen_e_acsl_k_16));
+          __gmpz_set(__gen_e_acsl_lambda_14,
+                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+          __gmpz_clear(__gen_e_acsl__10);
+        }
+        __gmpz_mul(__gen_e_acsl_accumulator_14,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_14),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_14));
+        /*@ assert
+            Eva: signed_overflow:
+              __gen_e_acsl_k_16 + __gen_e_acsl_one_14 ≤ 2147483647;
+        */
+        __gen_e_acsl_k_16 += __gen_e_acsl_one_14;
+      }
+    }
+    __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_13),
+                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_14));
+    __e_acsl_assert(__gen_e_acsl_eq_3 == 0,1,"Assertion","main",
+                    "\\product(-20, -1, \\lambda integer k; 2 * k) ==\n\\product(1, 20, \\lambda integer k; 2 * k)",
+                    "tests/arith/extended_quantifiers.c",28);
+    __gmpz_clear(__gen_e_acsl_lambda_13);
+    __gmpz_clear(__gen_e_acsl_accumulator_13);
+    __gmpz_clear(__gen_e_acsl_lambda_14);
+    __gmpz_clear(__gen_e_acsl_accumulator_14);
+  }
+  /*@
+  assert
+  \product(-20, -1, \lambda ℤ k; 2 * k) ≡
+  \product(1, 20, \lambda ℤ k; 2 * k); */
+  ;
+  __retres = 0;
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
deleted file mode 100644
index 362a4d3b1798252f52ecebda63c5101c8bfe6c56..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
+++ /dev/null
@@ -1,205 +0,0 @@
-/* Generated by Frama-C */
-#include "stddef.h"
-#include "stdio.h"
-extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-
-int main(void)
-{
-  int __retres;
-  unsigned long x = 4294967295UL;
-  int y = 10;
-  {
-    int __gen_e_acsl_k;
-    int __gen_e_acsl_one;
-    int __gen_e_acsl_cond;
-    int __gen_e_acsl_lambda;
-    int __gen_e_acsl_sum;
-    __gen_e_acsl_one = 1;
-    __gen_e_acsl_cond = 0;
-    __gen_e_acsl_lambda = 0;
-    __gen_e_acsl_sum = 0;
-    __gen_e_acsl_k = 2;
-    while (1) {
-      __gen_e_acsl_cond = __gen_e_acsl_k > 10;
-      if (__gen_e_acsl_cond) break;
-      else {
-        __gen_e_acsl_lambda = 2 * __gen_e_acsl_k;
-        __gen_e_acsl_sum += __gen_e_acsl_lambda;
-        __gen_e_acsl_k += __gen_e_acsl_one;
-      }
-    }
-    __e_acsl_assert(__gen_e_acsl_sum == 108,1,"Assertion","main",
-                    "\\sum(2, 10, \\lambda integer k; 2 * k) == 108",
-                    "tests/arith/sum.i",10);
-  }
-  /*@ assert \sum(2, 10, \lambda ℤ k; 2 * k) ≡ 108; */ ;
-  {
-    int __gen_e_acsl_k_2;
-    int __gen_e_acsl_one_2;
-    int __gen_e_acsl_cond_2;
-    __e_acsl_mpz_t __gen_e_acsl_lambda_2;
-    __e_acsl_mpz_t __gen_e_acsl_sum_2;
-    __e_acsl_mpz_t __gen_e_acsl__2;
-    int __gen_e_acsl_ne;
-    __gen_e_acsl_one_2 = 1;
-    __gen_e_acsl_cond_2 = 0;
-    __gmpz_init_set_si(__gen_e_acsl_lambda_2,0L);
-    __gmpz_init_set_si(__gen_e_acsl_sum_2,0L);
-    __gen_e_acsl_k_2 = 2;
-    while (1) {
-      __gen_e_acsl_cond_2 = __gen_e_acsl_k_2 > 35;
-      if (__gen_e_acsl_cond_2) break;
-      else {
-        {
-          __e_acsl_mpz_t __gen_e_acsl_;
-          __gmpz_init_set_ui(__gen_e_acsl_,18446744073709551615UL);
-          __gmpz_set(__gen_e_acsl_lambda_2,
-                     (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
-          __gmpz_clear(__gen_e_acsl_);
-        }
-        __gmpz_add(__gen_e_acsl_sum_2,
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_sum_2),
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_2));
-        __gen_e_acsl_k_2 += __gen_e_acsl_one_2;
-      }
-    }
-    __gmpz_init_set_si(__gen_e_acsl__2,0L);
-    __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sum_2),
-                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
-    __e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","main",
-                    "\\sum(2, 35, \\lambda integer k; 18446744073709551615) != 0",
-                    "tests/arith/sum.i",12);
-    __gmpz_clear(__gen_e_acsl_lambda_2);
-    __gmpz_clear(__gen_e_acsl_sum_2);
-    __gmpz_clear(__gen_e_acsl__2);
-  }
-  /*@ assert \sum(2, 35, \lambda ℤ k; 18446744073709551615) ≢ 0; */ ;
-  {
-    int __gen_e_acsl_k_3;
-    int __gen_e_acsl_one_3;
-    int __gen_e_acsl_cond_3;
-    int __gen_e_acsl_lambda_3;
-    int __gen_e_acsl_sum_3;
-    __gen_e_acsl_one_3 = 1;
-    __gen_e_acsl_cond_3 = 0;
-    __gen_e_acsl_lambda_3 = 0;
-    __gen_e_acsl_sum_3 = 0;
-    __gen_e_acsl_k_3 = 10;
-    while (1) {
-      __gen_e_acsl_cond_3 = __gen_e_acsl_k_3 > 2;
-      if (__gen_e_acsl_cond_3) break;
-      else {
-        __gen_e_acsl_lambda_3 = __gen_e_acsl_k_3;
-        __gen_e_acsl_sum_3 += __gen_e_acsl_lambda_3;
-        __gen_e_acsl_k_3 += __gen_e_acsl_one_3;
-      }
-    }
-    __e_acsl_assert(__gen_e_acsl_sum_3 == 0,1,"Assertion","main",
-                    "\\sum(10, 2, \\lambda integer k; k) == 0",
-                    "tests/arith/sum.i",14);
-  }
-  /*@ assert \sum(10, 2, \lambda ℤ k; k) ≡ 0; */ ;
-  {
-    __e_acsl_mpz_t __gen_e_acsl_x;
-    __e_acsl_mpz_t __gen_e_acsl_mul;
-    __e_acsl_mpz_t __gen_e_acsl__3;
-    __e_acsl_mpz_t __gen_e_acsl_k_4;
-    __e_acsl_mpz_t __gen_e_acsl_one_4;
-    int __gen_e_acsl_cond_4;
-    __e_acsl_mpz_t __gen_e_acsl_lambda_4;
-    __e_acsl_mpz_t __gen_e_acsl_sum_4;
-    __e_acsl_mpz_t __gen_e_acsl__4;
-    int __gen_e_acsl_eq;
-    __gmpz_init_set_ui(__gen_e_acsl_x,x);
-    __gmpz_init(__gen_e_acsl_mul);
-    __gmpz_mul(__gen_e_acsl_mul,
-               (__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
-               (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
-    __gmpz_init_set_si(__gen_e_acsl__3,2L);
-    __gmpz_init_set_si(__gen_e_acsl_one_4,1L);
-    __gen_e_acsl_cond_4 = 0;
-    __gmpz_init_set_si(__gen_e_acsl_lambda_4,0L);
-    __gmpz_init_set_si(__gen_e_acsl_sum_4,0L);
-    __gmpz_init_set(__gen_e_acsl_k_4,
-                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
-    while (1) {
-      __gen_e_acsl_cond_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
-                                       (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
-      if (__gen_e_acsl_cond_4 > 0) break;
-      else {
-        __gmpz_set(__gen_e_acsl_lambda_4,
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4));
-        __gmpz_add(__gen_e_acsl_sum_4,
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_sum_4),
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_4));
-        __gmpz_add(__gen_e_acsl_k_4,
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_4));
-      }
-    }
-    __gmpz_init_set_si(__gen_e_acsl__4,0L);
-    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sum_4),
-                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
-    __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main",
-                    "\\sum(x * x, 2, \\lambda integer k; k) == 0",
-                    "tests/arith/sum.i",16);
-    __gmpz_clear(__gen_e_acsl_x);
-    __gmpz_clear(__gen_e_acsl_mul);
-    __gmpz_clear(__gen_e_acsl__3);
-    __gmpz_clear(__gen_e_acsl_k_4);
-    __gmpz_clear(__gen_e_acsl_one_4);
-    __gmpz_clear(__gen_e_acsl_lambda_4);
-    __gmpz_clear(__gen_e_acsl_sum_4);
-    __gmpz_clear(__gen_e_acsl__4);
-  }
-  /*@ assert \sum(x * x, 2, \lambda ℤ k; k) ≡ 0; */ ;
-  {
-    __e_acsl_mpz_t __gen_e_acsl__5;
-    __e_acsl_mpz_t __gen_e_acsl__6;
-    __e_acsl_mpz_t __gen_e_acsl_k_5;
-    __e_acsl_mpz_t __gen_e_acsl_one_5;
-    int __gen_e_acsl_cond_5;
-    int __gen_e_acsl_lambda_5;
-    int __gen_e_acsl_sum_5;
-    __gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551610UL);
-    __gmpz_init_set_ui(__gen_e_acsl__6,18446744073709551615UL);
-    __gmpz_init_set_si(__gen_e_acsl_one_5,1L);
-    __gen_e_acsl_cond_5 = 0;
-    __gen_e_acsl_lambda_5 = 0;
-    __gen_e_acsl_sum_5 = 0;
-    __gmpz_init_set(__gen_e_acsl_k_5,
-                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
-    while (1) {
-      __gen_e_acsl_cond_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
-                                       (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
-      if (__gen_e_acsl_cond_5 > 0) break;
-      else {
-        __gen_e_acsl_lambda_5 = 1;
-        /*@ assert
-            Eva: signed_overflow:
-              __gen_e_acsl_sum_5 + __gen_e_acsl_lambda_5 ≤ 2147483647;
-        */
-        __gen_e_acsl_sum_5 += __gen_e_acsl_lambda_5;
-        __gmpz_add(__gen_e_acsl_k_5,
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
-                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_5));
-      }
-    }
-    __e_acsl_assert(__gen_e_acsl_sum_5 == 6,1,"Assertion","main",
-                    "\\sum(18446744073709551610, 18446744073709551615, \\lambda integer k; 1) == 6",
-                    "tests/arith/sum.i",18);
-    __gmpz_clear(__gen_e_acsl__5);
-    __gmpz_clear(__gen_e_acsl__6);
-    __gmpz_clear(__gen_e_acsl_k_5);
-    __gmpz_clear(__gen_e_acsl_one_5);
-  }
-  /*@
-  assert
-  \sum(18446744073709551610, 18446744073709551615, \lambda ℤ k; 1) ≡ 6;
-   */
-  ;
-  __retres = 0;
-  return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
deleted file mode 100644
index df0b0c5c271fba45ac9f080c494664c60e65f105..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
+++ /dev/null
@@ -1,16 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/sum.i:10: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:12: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/sum.i:12: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:14: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:16: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/sum.i:16: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:18: Warning: 
-  signed overflow.
-  assert __gen_e_acsl_sum_5 + __gen_e_acsl_lambda_5 ≤ 2147483647;
-[eva:alarm] tests/arith/sum.i:18: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/sum.i:18: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/sum.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/extended_quantifiers.e-acsl.err.log
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle_dev/sum.e-acsl.err.log
rename to src/plugins/e-acsl/tests/arith/oracle_dev/extended_quantifiers.e-acsl.err.log
diff --git a/src/plugins/e-acsl/tests/arith/sum.i b/src/plugins/e-acsl/tests/arith/sum.i
deleted file mode 100644
index 3737ad347a01d3413e4193a1d408d75902f98522..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/sum.i
+++ /dev/null
@@ -1,22 +0,0 @@
-/* run.config
-   COMMENT: sum operations
-   STDOPT: +"-eva-precision=3"
-*/
-
-int main(void) {
-  unsigned long x = 4294967295UL;
-  int y = 10;
-
-  /*@ assert \sum(2,10,\lambda integer k; 2*k) == 108; */;
-
-  /*@ assert \sum(2,35,\lambda integer k; 18446744073709551615) != 0; */;
-
-  /*@ assert \sum(10,2,\lambda integer k; k) == 0; */;
-
-  /*@ assert \sum(x*x,2,\lambda integer k; k) == 0; */;
-
-  /*@ assert \sum(18446744073709551610,18446744073709551615,\lambda integer k; 1) == 6; */
-  ;
-
-  return 0;
-}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 9fb4c16aade02563c58460cb4e2c550226670a81..1a7afd5bee9eaa585b2e079469cfdabf548079f3 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -524,9 +524,9 @@ void __e_acsl_globals_init(void)
                          sizeof("tests/builtin/strcat.c:70"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
-    __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:68";
+    __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:69";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
-                         sizeof("tests/builtin/strcat.c:68"));
+                         sizeof("tests/builtin/strcat.c:69"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
     __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:67";
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index efdc2598cce8391acafe3d49815570995fec492d..44170551c065847fe09d7c0e1cebbfc1f4e0d11b 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -286,14 +286,14 @@ void __e_acsl_globals_init(void)
                          sizeof("tests/builtin/strlen.c:33"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
-    __gen_e_acsl_literal_string_14 = "tests/builtin/strlen.c:30";
+    __gen_e_acsl_literal_string_14 = "tests/builtin/strlen.c:31";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
-                         sizeof("tests/builtin/strlen.c:30"));
+                         sizeof("tests/builtin/strlen.c:31"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
-    __gen_e_acsl_literal_string_13 = "tests/builtin/strlen.c:28";
+    __gen_e_acsl_literal_string_13 = "tests/builtin/strlen.c:29";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
-                         sizeof("tests/builtin/strlen.c:28"));
+                         sizeof("tests/builtin/strlen.c:29"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
     __gen_e_acsl_literal_string_12 = "tests/builtin/strlen.c:24";
@@ -311,9 +311,9 @@ void __e_acsl_globals_init(void)
                          sizeof("tests/builtin/strlen.c:22"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
-    __gen_e_acsl_literal_string_9 = "tests/builtin/strlen.c:20";
+    __gen_e_acsl_literal_string_9 = "tests/builtin/strlen.c:21";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
-                         sizeof("tests/builtin/strlen.c:20"));
+                         sizeof("tests/builtin/strlen.c:21"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
     __gen_e_acsl_literal_string = "TEST %d: ";
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index f6d5a49bb4668f287960d7a34c241cda92310917..077e7e1b7111003c5ae82c748c084ea16eaf0819 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -45,8 +45,12 @@
   E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning: 
+  E-ACSL construct `logic functions or predicates with labels'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
+  E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: 
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 1ceb9a53ba6c92b671944c932ca575728419a8e4..406978ac5f39a280b111b1dc00a11a06c240af64 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -39,8 +39,12 @@
   E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning: 
+  E-ACSL construct `logic functions or predicates with labels'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
+  E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: 
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 63fab70b9482fd6e1cf972c850956812b2008ff3..b1e0c13ab7c0c81ddca966a75862fbafdb2ce343 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -42,8 +42,12 @@
   E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning: 
+  E-ACSL construct `logic functions or predicates with labels'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
+  E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: 
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
index 9e0fa5e56b2f4f4c39d44078054968dd50711b45..ba266124594f7cb22a17928de0f6f61f45e81758 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
@@ -1,5 +1,5 @@
 TEST 1: OK: Expected execution at tests/builtin/strcat.c:67
-TEST 2: OK: Expected execution at tests/builtin/strcat.c:68
+TEST 2: OK: Expected execution at tests/builtin/strcat.c:69
 strcat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
 TEST 3: OK: Expected signal at tests/builtin/strcat.c:70
 strcat: destination string string unallocated
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log
index 4a74fec3e9162c9a27c2646b92417cf7c6b9b8e8..12fc549bbd1f81e6d55a9ff66150154bf9fcbc34 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log
@@ -1,10 +1,10 @@
-TEST 1: OK: Expected execution at tests/builtin/strlen.c:20
+TEST 1: OK: Expected execution at tests/builtin/strlen.c:21
 TEST 2: OK: Expected execution at tests/builtin/strlen.c:22
 TEST 3: OK: Expected execution at tests/builtin/strlen.c:23
 TEST 4: OK: Expected execution at tests/builtin/strlen.c:24
 strlen: input string not NUL-terminated
-TEST 5: OK: Expected signal at tests/builtin/strlen.c:28
+TEST 5: OK: Expected signal at tests/builtin/strlen.c:29
 strlen: input string not NUL-terminated
-TEST 6: OK: Expected signal at tests/builtin/strlen.c:30
+TEST 6: OK: Expected signal at tests/builtin/strlen.c:31
 strlen: input string unallocated
 TEST 7: OK: Expected signal at tests/builtin/strlen.c:33
diff --git a/src/plugins/e-acsl/tests/builtin/strcat.c b/src/plugins/e-acsl/tests/builtin/strcat.c
index 2c4888ccb582a2161714936c998d05712b08e207..1e9c506bcc3a393d79f8112fe2b0abc559b44031 100644
--- a/src/plugins/e-acsl/tests/builtin/strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/strcat.c
@@ -65,8 +65,8 @@ int main(int argc, const char **argv) {
 
     /* strcat */
     OK(strcat(dest1, const_str)); // enough space in dest [ok]
-    OK(strcat(dest3,
-              empty_str)); // enough space in dest (concat with empty) [ok]
+    // enough space in dest (concat with empty) [ok]:
+    OK(strcat(dest3, empty_str));
     ABRT(strcat(dest2, const_str));       // insufficient space in dest [abort]
     ABRT(strcat(unalloc_str, const_str)); // unallocated in dest [abort]
     ABRT(strcat(dest2, unalloc_str));     // unallocated in src [abort]
diff --git a/src/plugins/e-acsl/tests/builtin/strlen.c b/src/plugins/e-acsl/tests/builtin/strlen.c
index fa4b27884db767f43d747ca5010e83344d046045..b7ef400329cd543aedbe5277f2db0e6cb1b1b791 100644
--- a/src/plugins/e-acsl/tests/builtin/strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/strlen.c
@@ -17,18 +17,18 @@ int main(int argc, const char **argv) {
   char stack_str[] = "the dog";
   char *const_str = "the hog";
 
-  OK(EQ(len = strlen(empty_str),
-        0)); // strlen on a valid (zero-length) string [ok]
+  // strlen on a valid (zero-length) string [ok]:
+  OK(EQ(len = strlen(empty_str), 0));
   OK(EQ(len = strlen(heap_str), 7));  // strlen on a heap string [ok]
   OK(EQ(len = strlen(stack_str), 7)); // strlen on a stack string [ok]
   OK(EQ(len = strlen(const_str), 7)); // strlen on a const string [ok]
 
   heap_str[7] = 'a';
   stack_str[7] = 'a';
-  ABRT(EQ(len = strlen(heap_str),
-          7)); // strlen on unterminated heap string [abort]
-  ABRT(EQ(len = strlen(stack_str),
-          7)); // strlen on unterminated stack string [abort]
+  // strlen on unterminated heap string [abort]:
+  ABRT(EQ(len = strlen(heap_str), 7));
+  // strlen on unterminated stack string [abort]:
+  ABRT(EQ(len = strlen(stack_str), 7));
   free(heap_str);
   ABRT(EQ(len = strlen(heap_str), 7)); // strlen on invalid heap string [abort]
   return 0;
diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c
index 87178190a11e980881a6d02ec4f09235a212752b..41f91017210623d6199c28c04a5db79b2be7f384 100644
--- a/src/plugins/e-acsl/tests/format/fprintf.c
+++ b/src/plugins/e-acsl/tests/format/fprintf.c
@@ -44,7 +44,7 @@ int main(int argc, const char **argv) {
   ABRT(snprintf(pstr, 6, "-%s-", "123")); // try read-only
   ABRT(snprintf(buf, 6, "-%s-", "123"));  // not enough space
   ABRT(snprintf(NULL, 6, "-%s-", "123")); // not enough space
-  OK(snprintf(NULL, 0, "-%s-",
-              "123")); // NULL should be file because of 0 chars to write
+  // NULL should be fine because of 0 chars to write:
+  OK(snprintf(NULL, 0, "-%s-", "123"));
   return 0;
 }
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index f4162a6fb7f8549e89fe6e56050f35839605ffcc..0fb3e03f963f1ca84c2d99208f7a971bf4e3ab08 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -252,9 +252,9 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:47";
+    __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:48";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
-                         sizeof("tests/format/fprintf.c:47"));
+                         sizeof("tests/format/fprintf.c:48"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
     __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:46";
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
index 0bbf23ea140d1b32644f3a7749bfb189bdf52cff..ee17e51614be3d7c41048a9df75c551798d663be 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
@@ -25,4 +25,4 @@ sprintf: output buffer is unallocated or has insufficient length to store 6 char
 TEST 16: OK: Expected signal at tests/format/fprintf.c:45
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
 TEST 17: OK: Expected signal at tests/format/fprintf.c:46
-TEST 18: OK: Expected execution at tests/format/fprintf.c:47
+TEST 18: OK: Expected execution at tests/format/fprintf.c:48
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
index b2c6ce5637bbcb55dce5e172f6a0932fef9fc422..476e946ba75399bcc809e56f6827a993e559e38e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -14,8 +14,12 @@
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: 
   E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning: 
+  E-ACSL construct `logic functions or predicates with labels'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
+  E-ACSL construct `logic functions or predicates with labels'
   is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: