diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index c1cb87fa3618033deefec4c588ad7d0b9ceb6762..8ee13e2c4fef29c60271f4cafe77da9f08021d23 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -240,6 +240,9 @@ let add_old = add_logic Logic_const.old_label
 let add_init state =
   add_logic Logic_const.init_label (Db.Value.globals_state ()) state
 
+let add_logic_var env lv cvalue =
+  { env with logic_vars = LogicVarEnv.add lv cvalue env.logic_vars }
+
 let make_env logic_env state =
   let transfer label map =
     Logic_label.Map.add label (logic_env.Abstract_domain.states label) map
@@ -459,6 +462,12 @@ type 'a eval_result = {
   ldeps: logic_deps;
 }
 
+let join_eval_result r1 r2 =
+  let eover = Cvalue.V.join r2.eover r1.eover in
+  let eunder = Cvalue.V.meet r1.eunder r2.eunder in
+  let ldeps = join_logic_deps r1.ldeps r2.ldeps in
+  { eover; eunder; ldeps; etype = r1.etype; empty = r1.empty || r2.empty; }
+
 (* When computing an under-approximation, we make the hypothesis that the state
    is not Bottom. Hence, over-approximations of cardinal <= 1 are actually of
    cardinal 1, and are thus exact. *)
@@ -1361,18 +1370,31 @@ and eval_known_logic_function ~alarm_mode env li labels args =
       with Cvalue.V.Not_based_on_null -> c_alarm ()
     end
 
-  | "\\min", Some Linteger, _, [t1; t2] ->
-    let backward = Cvalue.V.backward_comp_int_left Comp.Le in
-    eval_extremum Cil.intType backward ~alarm_mode env t1 t2
-  | "\\max", Some Linteger, _, [t1; t2] ->
-    let backward = Cvalue.V.backward_comp_int_left Comp.Ge in
-    eval_extremum Cil.intType backward ~alarm_mode env t1 t2
-  | "\\min", Some Lreal, _, [t1; t2] ->
-    let backward = Cvalue.V.backward_comp_float_left_true Comp.Le Fval.Real in
-    eval_extremum Cil.floatType backward ~alarm_mode env t1 t2
-  | "\\max", Some Lreal, _, [t1; t2] ->
-    let backward = Cvalue.V.backward_comp_float_left_true Comp.Ge Fval.Real in
-    eval_extremum Cil.doubleType backward ~alarm_mode env t1 t2
+  | ("\\min" | "\\max"), Some typ, _, t1 :: t2 :: tail_args ->
+    begin
+      let comp = if lvi.lv_name = "\\min" then Comp.Le else Comp.Ge in
+      let backward =
+        match typ with
+        | Linteger -> Cvalue.V.backward_comp_int_left comp
+        | Lreal -> Cvalue.V.backward_comp_float_left_true comp Fval.Real
+        | _ -> assert false
+      in
+      let r1 = eval_term ~alarm_mode env t1
+      and r2 = eval_term ~alarm_mode env t2 in
+      (* If there are 2 arguments, it is the mathematical function \min or \max.
+         If there are 3, it is the ACSL extended quantifiers \min or \max. *)
+      match tail_args with
+      | [] -> compute_extremum backward r1 r2
+      | [ { term_node = Tlambda ([lv], term) } ] ->
+        (* Evaluation of [term] when the logic variable [lv] is in [cvalue]. *)
+        let eval_term cvalue =
+          let env = add_logic_var env lv cvalue in
+          eval_term ~alarm_mode env term
+        in
+        eval_quantifier_extremum backward ~min:r1 ~max:r2 eval_term
+      | _ -> assert false
+    end
+
   | _ -> assert false
 
 and eval_float_builtin_arity2  ~alarm_mode env name arg1 arg2 =
@@ -1401,19 +1423,68 @@ and eval_float_builtin_arity2  ~alarm_mode env name arg1 arg2 =
   let ldeps = join_logic_deps r1.ldeps r2.ldeps in
   { etype = r1.etype; eunder; eover = v; ldeps; empty = r1.empty || r2.empty; }
 
-(* Evaluates the max (resp. the min) between the terms [t1] and [t2],
+
+(* Computes the max (resp. the min) between the evaluation results [r1] and [r2]
    according to [backward_left v1 v2] that reduces [v1] by assuming it is
    greater than (resp. lower than) [v2]. *)
-and eval_extremum etype backward_left ~alarm_mode env t1 t2 =
-  let r1 = eval_term ~alarm_mode env t1
-  and r2 = eval_term ~alarm_mode env t2 in
-  let reduced_v1 = backward_left r1.eover r2.eover
-  and reduced_v2 = backward_left r2.eover r1.eover in
-  let eover = Cvalue.V.join reduced_v1 reduced_v2 in
-  let eunder = Cvalue.V.meet r1.eunder r2.eunder in
-  let ldeps = join_logic_deps r1.ldeps r2.ldeps in
-  {eover; eunder; ldeps; etype; empty = r1.empty || r2.empty; }
-
+and compute_extremum backward_left r1 r2 =
+  let r1 = { r1 with eover = backward_left r1.eover r2.eover }
+  and r2 = { r2 with eover = backward_left r2.eover r1.eover } in
+  join_eval_result r1 r2
+
+(* Evaluates ACSL extended quantifiers \max or \min: computes (an approximation
+   of) the max (resp. the min) of [eval_term i] when [i] ranges between [min]
+   and [max], according to [backward_left v1 v2] that reduces [v1] by assuming
+   it is greater (resp. lower) than [v2]. *)
+and eval_quantifier_extremum backward_left ~min ~max eval_term =
+  (* Returns [r] as the result, with updated [empty] and [ldeps] fields. *)
+  let return r =
+    let ldeps = join_logic_deps r.ldeps (join_logic_deps min.ldeps max.ldeps) in
+    let empty = min.empty || max.empty || r.empty in
+    { r with ldeps; empty; }
+  in
+  let eval_ival ival = eval_term (Cvalue.V.inject_ival ival) in
+  let project r = Cvalue.V.project_ival r.eover in
+  match Ival.min_and_max (project min),
+        Ival.min_and_max (project max) with
+  | (min, Some b), (Some e, max) when Integer.le b e ->
+    (* All integers between [b] and [e] are necessarily in the range to be
+       considered. If [e-b] is small enough, evaluate [eval_term i] for each [i]
+       between [b] and [e]. Otherwise, evaluate [eval_term] for the bound [b]
+       and [e], and for the interval [b+1..e-1]. We could be more precise by
+       subdividing the interval. *)
+    let r =
+      if Integer.equal e b
+      then eval_term (Cvalue.V.inject_int b)
+      else
+        let fold =
+          if Integer.(le (sub e b) (of_int 10))
+          then Ival.fold_enum
+          else Ival.fold_int_bounds
+        in
+        let ival = Ival.inject_range (Some b) (Some e) in
+        let list = fold (fun i acc -> eval_ival i :: acc) ival [] in
+        (* Reduce each result to only keep the possible extrema. *)
+        let hd, tl = List.hd list, List.tl list in
+        List.fold_left (compute_extremum backward_left) hd tl
+    in
+    (* Integers below [b] and above [e] may not be in the range to be considered,
+       so we can't reduce [r] according to them. However, we must join to [r]
+       the evaluation of [eval_term] for these integers, and we can reduce
+       these evaluations to only keep results greater (or lower, according to
+       [backward_left]) than [r]. *)
+    let below = eval_ival (Ival.inject_range min (Some (Integer.pred b)))
+    and above = eval_ival (Ival.inject_range (Some (Integer.succ e)) max) in
+    let below = { below with eover = backward_left below.eover r.eover }
+    and above = { above with eover = backward_left above.eover r.eover } in
+    join_eval_result r (join_eval_result below above)
+  | (b, _), (_, e) ->
+    (* If [min] can be greater than [max], the result is unspecified. *)
+    let r = eval_ival (Ival.inject_range b e) in
+    return { r with eover = Cvalue.V.top; eunder = Cvalue.V.bottom }
+  | exception Cvalue.V.Not_based_on_null ->
+    let r = eval_term (Cvalue.V.join min.eover max.eover) in
+    return { r with eover = Cvalue.V.top; eunder = Cvalue.V.bottom }
 
 let eval_tlval_as_location ~alarm_mode env t =
   let r = eval_term_as_lval ~alarm_mode env t in
@@ -1814,8 +1885,7 @@ let reduce_by_left_relation ~alarm_mode env positive tl rel tr =
       let reduce = Eval_op.backward_comp_left_from_type logic_var.lv_type in
       let cvalue = reduce positive comp cvalue cond_v in
       if V.is_bottom cvalue then raise Reduce_to_bottom;
-      let logic_vars = LogicVarEnv.add logic_var cvalue env.logic_vars in
-      { env with logic_vars }
+      add_logic_var env logic_var cvalue
     | Location (typ_loc, locs) ->
       let reduce = Eval_op.backward_comp_left_from_type (Ctype typ_loc) in
       if debug then Format.printf "#Val right term %a@." V.pretty cond_v;
@@ -1937,8 +2007,7 @@ let reduce_by_known_papp ~alarm_mode env positive li _labels args =
         let vl = LogicVarEnv.find logic_var env.logic_vars in
         let reduced = Cvalue.V.narrow vl vr in
         if V.equal V.bottom reduced then raise Reduce_to_bottom;
-        let logic_vars = LogicVarEnv.add logic_var reduced env.logic_vars in
-        { env with logic_vars }
+        add_logic_var env logic_var reduced
       | Location (_typ, locsl) ->
         let aux locl env =
           let state = env_current_state env in
diff --git a/tests/value/logic.c b/tests/value/logic.c
index 9ba0bf437d48621353f33ea92f8749c3f9ba9726..e5963edcd24c29b6ccdbf20c6bcd2bbff4b0466c 100644
--- a/tests/value/logic.c
+++ b/tests/value/logic.c
@@ -308,6 +308,52 @@ void check_and_assert () {
   }
 }
 
+/* Tests the ACSL extended quantifiers \min and \max. */
+void min_max_quantifier () {
+  int i, j, t[64];
+  /*@ loop unroll 32; */
+  for (i = 0; i < 32; i++)
+    t[i] = i;
+  t[32] = 0;
+  /*@ loop unroll 32; */
+  for (i = 33; i < 64; i++)
+    t[i] = 64-i;
+  /*@ check valid: \max(12, 12, \lambda integer i; t[i]) == 12; */
+  /*@ check valid: \min(12, 12, \lambda integer i; t[i]) == 12; */
+  /*@ check valid: \max(28, 36, \lambda integer i; t[i]) == 31; */
+  /*@ check valid: \min(28, 36, \lambda integer i; t[i]) == 0; */
+  /*@ check valid: \max(2, 30, \lambda integer i; t[i]) == 30; */
+  /*@ check valid: \min(2, 30, \lambda integer i; t[i]) == 2; */
+  /*@ check valid: \max(16, 48, \lambda integer i; t[i]) == 31; */
+  /*@ check valid: \min(16, 48, \lambda integer i; t[i]) == 0; */
+  /*@ check unknown: \max(11, 10, \lambda integer i; t[i]) >= 0; */
+  /*@ check unknown: \min(11, 10, \lambda integer i; t[i]) >= 0; */
+  i = Frama_C_interval(2,5);
+  j = Frama_C_interval(10, 12);
+  /*@ check valid: \max(i, j, \lambda integer i; t[i]) >= 10; */
+  /*@ check valid: \max(i, j, \lambda integer i; t[i]) <= 12; */
+  /*@ check valid: \min(i, j, \lambda integer i; t[i]) >= 2; */
+  /*@ check valid: \min(i, j, \lambda integer i; t[i]) <= 5; */
+  /*@ check unknown: \max(i, j, \lambda integer i; t[i]) > 10; */
+  /*@ check unknown: \max(i, j, \lambda integer i; t[i]) < 12; */
+  /*@ check unknown: \min(i, j, \lambda integer i; t[i]) > 2; */
+  /*@ check unknown: \min(i, j, \lambda integer i; t[i]) < 5; */
+  i = Frama_C_interval(2,8);
+  j = Frama_C_interval(16, 30);
+  /*@ check valid: \max(i, j, \lambda integer i; t[i]) >= 16; */
+  /*@ check valid: \max(i, j, \lambda integer i; t[i]) <= 30; */
+  /*@ check valid: \min(i, j, \lambda integer i; t[i]) >= 2; */
+  /*@ check valid: \min(i, j, \lambda integer i; t[i]) <= 8; */
+  /*@ check unknown: \max(i, j, \lambda integer i; t[i]) > 16; */
+  /*@ check unknown: \max(i, j, \lambda integer i; t[i]) < 30; */
+  /*@ check unknown: \min(i, j, \lambda integer i; t[i]) > 2; */
+  /*@ check unknown: \min(i, j, \lambda integer i; t[i]) < 8; */
+  i = Frama_C_interval(4,16);
+  j = Frama_C_interval(12, 24);
+  /*@ check unknown: \max(i, j, \lambda integer i; t[i]) >= 0; */
+  /*@ check unknown: \min(i, j, \lambda integer i; t[i]) >= 0; */
+}
+
 void main () {
   eq_tsets();
   eq_char();
@@ -321,4 +367,5 @@ void main () {
   min_max();
   assign_tsets();
   check_and_assert ();
+  min_max_quantifier ();
 }
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index 99b0604e3a83ad03a8dd2fe61601cb152b69111a..7f1e124d0e9ada972519f8652deac34560e17adb 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -14,7 +14,7 @@
   arr_ptr[0..2] ∈ {0}
   arr_ptr_arr[0..5] ∈ {0}
 [eva] computing for function eq_tsets <- main.
-  Called from tests/value/logic.c:312.
+  Called from tests/value/logic.c:358.
 [eva] tests/value/logic.c:103: 
   cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
 [eva:alarm] tests/value/logic.c:103: Warning: assertion got status unknown.
@@ -56,20 +56,20 @@
 [eva] Recording results for eq_tsets
 [eva] Done for function eq_tsets
 [eva] computing for function eq_char <- main.
-  Called from tests/value/logic.c:313.
+  Called from tests/value/logic.c:359.
 [eva] tests/value/logic.c:149: Frama_C_show_each: {-126}
 [eva] tests/value/logic.c:150: assertion got status valid.
 [eva] tests/value/logic.c:151: assertion got status valid.
 [eva] Recording results for eq_char
 [eva] Done for function eq_char
 [eva] computing for function casts <- main.
-  Called from tests/value/logic.c:314.
+  Called from tests/value/logic.c:360.
 [eva] tests/value/logic.c:155: assertion got status valid.
 [eva] tests/value/logic.c:156: assertion got status valid.
 [eva] Recording results for casts
 [eva] Done for function casts
 [eva] computing for function empty_tset <- main.
-  Called from tests/value/logic.c:315.
+  Called from tests/value/logic.c:361.
 [eva] computing for function f_empty_tset <- empty_tset <- main.
   Called from tests/value/logic.c:166.
 [eva] using specification for function f_empty_tset
@@ -82,7 +82,7 @@
 [eva] Recording results for empty_tset
 [eva] Done for function empty_tset
 [eva] computing for function reduce_by_equal <- main.
-  Called from tests/value/logic.c:316.
+  Called from tests/value/logic.c:362.
 [eva:alarm] tests/value/logic.c:172: Warning: 
   accessing out of bounds index. assert 0 ≤ v;
 [eva:alarm] tests/value/logic.c:172: Warning: 
@@ -92,7 +92,7 @@
 [eva] Recording results for reduce_by_equal
 [eva] Done for function reduce_by_equal
 [eva] computing for function alarms <- main.
-  Called from tests/value/logic.c:317.
+  Called from tests/value/logic.c:363.
 [eva:alarm] tests/value/logic.c:182: Warning: 
   assertion 'ASSUME' got status unknown.
 [eva:alarm] tests/value/logic.c:184: Warning: 
@@ -124,7 +124,7 @@
 [eva] Recording results for alarms
 [eva] Done for function alarms
 [eva] computing for function cond_in_lval <- main.
-  Called from tests/value/logic.c:318.
+  Called from tests/value/logic.c:364.
 [eva] computing for function select_like <- cond_in_lval <- main.
   Called from tests/value/logic.c:228.
 [eva] using specification for function select_like
@@ -152,7 +152,7 @@
 [eva] Recording results for cond_in_lval
 [eva] Done for function cond_in_lval
 [eva] computing for function pred <- main.
-  Called from tests/value/logic.c:319.
+  Called from tests/value/logic.c:365.
 [eva] tests/value/logic.c:90: assertion got status valid.
 [eva] tests/value/logic.c:91: assertion got status valid.
 [eva] tests/value/logic.c:31: 
@@ -201,7 +201,7 @@
 [eva] Recording results for pred
 [eva] Done for function pred
 [eva] computing for function float_sign <- main.
-  Called from tests/value/logic.c:320.
+  Called from tests/value/logic.c:366.
 [eva] tests/value/logic.c:251: assertion got status valid.
 [eva] tests/value/logic.c:252: assertion got status valid.
 [eva] tests/value/logic.c:253: assertion got status valid.
@@ -210,7 +210,7 @@
 [eva] Recording results for float_sign
 [eva] Done for function float_sign
 [eva] computing for function min_max <- main.
-  Called from tests/value/logic.c:321.
+  Called from tests/value/logic.c:367.
 [eva] computing for function Frama_C_interval <- min_max <- main.
   Called from tests/value/logic.c:274.
 [eva] using specification for function Frama_C_interval
@@ -235,7 +235,7 @@
 [eva] Recording results for min_max
 [eva] Done for function min_max
 [eva] computing for function assign_tsets <- main.
-  Called from tests/value/logic.c:322.
+  Called from tests/value/logic.c:368.
 [eva] computing for function assign_tsets_aux <- assign_tsets <- main.
   Called from tests/value/logic.c:269.
 [eva] using specification for function assign_tsets_aux
@@ -243,7 +243,7 @@
 [eva] Recording results for assign_tsets
 [eva] Done for function assign_tsets
 [eva] computing for function check_and_assert <- main.
-  Called from tests/value/logic.c:323.
+  Called from tests/value/logic.c:369.
 [eva:alarm] tests/value/logic.c:295: Warning: assertion got status unknown.
 [eva] tests/value/logic.c:296: Frama_C_show_each_42: {42}
 [eva] tests/value/logic.c:297: check got status valid.
@@ -257,6 +257,80 @@
 [eva] tests/value/logic.c:307: Frama_C_show_each_reachable: {42}
 [eva] Recording results for check_and_assert
 [eva] Done for function check_and_assert
+[eva] computing for function min_max_quantifier <- main.
+  Called from tests/value/logic.c:370.
+[eva] tests/value/logic.c:321: check 'valid' got status valid.
+[eva] tests/value/logic.c:322: check 'valid' got status valid.
+[eva] tests/value/logic.c:323: check 'valid' got status valid.
+[eva] tests/value/logic.c:324: check 'valid' got status valid.
+[eva] tests/value/logic.c:325: check 'valid' got status valid.
+[eva] tests/value/logic.c:326: check 'valid' got status valid.
+[eva:alarm] tests/value/logic.c:327: Warning: check 'valid' got status unknown.
+[eva:alarm] tests/value/logic.c:328: Warning: check 'valid' got status unknown.
+[eva:alarm] tests/value/logic.c:329: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:330: Warning: 
+  check 'unknown' got status unknown.
+[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
+  Called from tests/value/logic.c:331.
+[eva] tests/value/logic.c:331: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
+  Called from tests/value/logic.c:332.
+[eva] tests/value/logic.c:332: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/logic.c:333: check 'valid' got status valid.
+[eva] tests/value/logic.c:334: check 'valid' got status valid.
+[eva] tests/value/logic.c:335: check 'valid' got status valid.
+[eva] tests/value/logic.c:336: check 'valid' got status valid.
+[eva:alarm] tests/value/logic.c:337: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:338: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:339: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:340: Warning: 
+  check 'unknown' got status unknown.
+[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
+  Called from tests/value/logic.c:341.
+[eva] tests/value/logic.c:341: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
+  Called from tests/value/logic.c:342.
+[eva] tests/value/logic.c:342: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/logic.c:343: check 'valid' got status valid.
+[eva] tests/value/logic.c:344: check 'valid' got status valid.
+[eva] tests/value/logic.c:345: check 'valid' got status valid.
+[eva] tests/value/logic.c:346: check 'valid' got status valid.
+[eva:alarm] tests/value/logic.c:347: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:348: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:349: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:350: Warning: 
+  check 'unknown' got status unknown.
+[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
+  Called from tests/value/logic.c:351.
+[eva] tests/value/logic.c:351: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- min_max_quantifier <- main.
+  Called from tests/value/logic.c:352.
+[eva] tests/value/logic.c:352: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/logic.c:353: Warning: 
+  check 'unknown' got status unknown.
+[eva:alarm] tests/value/logic.c:354: Warning: 
+  check 'unknown' got status unknown.
+[eva] Recording results for min_max_quantifier
+[eva] Done for function min_max_quantifier
 [eva] Recording results for main
 [eva] done for function main
 [scope:rm_asserts] removing 5 assertion(s)
@@ -310,6 +384,74 @@
   a ∈ {0}
   b ∈ {-0.}
   d ∈ [-0. .. 0.]
+[eva:final-states] Values at end of function min_max_quantifier:
+  Frama_C_entropy_source ∈ [--..--]
+  i ∈ [4..16]
+  j ∈ [12..24]
+  t_0[0] ∈ {0}
+     [1] ∈ {1}
+     [2] ∈ {2}
+     [3] ∈ {3}
+     [4] ∈ {4}
+     [5] ∈ {5}
+     [6] ∈ {6}
+     [7] ∈ {7}
+     [8] ∈ {8}
+     [9] ∈ {9}
+     [10] ∈ {10}
+     [11] ∈ {11}
+     [12] ∈ {12}
+     [13] ∈ {13}
+     [14] ∈ {14}
+     [15] ∈ {15}
+     [16] ∈ {16}
+     [17] ∈ {17}
+     [18] ∈ {18}
+     [19] ∈ {19}
+     [20] ∈ {20}
+     [21] ∈ {21}
+     [22] ∈ {22}
+     [23] ∈ {23}
+     [24] ∈ {24}
+     [25] ∈ {25}
+     [26] ∈ {26}
+     [27] ∈ {27}
+     [28] ∈ {28}
+     [29] ∈ {29}
+     [30] ∈ {30}
+     [31] ∈ {31}
+     [32] ∈ {0}
+     [33] ∈ {31}
+     [34] ∈ {30}
+     [35] ∈ {29}
+     [36] ∈ {28}
+     [37] ∈ {27}
+     [38] ∈ {26}
+     [39] ∈ {25}
+     [40] ∈ {24}
+     [41] ∈ {23}
+     [42] ∈ {22}
+     [43] ∈ {21}
+     [44] ∈ {20}
+     [45] ∈ {19}
+     [46] ∈ {18}
+     [47] ∈ {17}
+     [48] ∈ {16}
+     [49] ∈ {15}
+     [50] ∈ {14}
+     [51] ∈ {13}
+     [52] ∈ {12}
+     [53] ∈ {11}
+     [54] ∈ {10}
+     [55] ∈ {9}
+     [56] ∈ {8}
+     [57] ∈ {7}
+     [58] ∈ {6}
+     [59] ∈ {5}
+     [60] ∈ {4}
+     [61] ∈ {3}
+     [62] ∈ {2}
+     [63] ∈ {1}
 [eva:final-states] Values at end of function reduce_by_equal:
   a[0..8] ∈ {1}
    [9] ∈ [--..--]
@@ -369,6 +511,8 @@
 [from] Computing for function Frama_C_interval <-min_max
 [from] Done for function Frama_C_interval
 [from] Done for function min_max
+[from] Computing for function min_max_quantifier
+[from] Done for function min_max_quantifier
 [from] Computing for function reduce_by_equal
 [from] Done for function reduce_by_equal
 [from] Computing for function cond_in_lval
@@ -415,6 +559,8 @@
   s1.f1 FROM \nothing
 [from] Function min_max:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function min_max_quantifier:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function reduce_by_equal:
   NO EFFECTS
 [from] Function select_like:
@@ -483,6 +629,10 @@
     Frama_C_entropy_source; x_0; y; z; r1; r2; r3; r4; a; b; d
 [inout] Inputs for function min_max:
     Frama_C_entropy_source; v
+[inout] Out (internal) for function min_max_quantifier:
+    Frama_C_entropy_source; i; j; t_0[0..63]
+[inout] Inputs for function min_max_quantifier:
+    Frama_C_entropy_source
 [inout] Out (internal) for function reduce_by_equal:
     a[0..9]
 [inout] Inputs for function reduce_by_equal: