diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index e6cd5f666aa72ff46198acbe3f1dbdc2f8b06d4c..ac50025173cccc8707fe4d6e5385fd79365d821c 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -25,8 +25,8 @@
    The limit is defined by the option -eva-auto-loop-unroll. *)
 
 (* Gist of the heuristic:
-   - find a loop exit condition, in the form of a statement "if(cond) break;".
-     such that exactly one lvalue [lval] in the condition [cond] is modified
+   - collect loop exit conditions [cond] from statements "if (cond) break;"
+   - find a loop exit condition in which only one lvalue [lval] is modified
      within the loop; all other lvalues must be constant in the loop.
    - find a value [v_exit] such that [lval] ∈ [v_exit] ⇒ [cond] holds.
    - evaluate [lval] to its initial value [v_init] in the loop entry state.
@@ -34,7 +34,7 @@
      iteration of the loop.
 
    If [v_init] + k × [v_delta] ⊂ [v_exit], then the number of iterations
-   is bounded by the limit [k].
+   is bounded by [k].
 
    The heuristic is syntactic and limited to the current function: it does not
    handle assignment through pointers or function calls.
@@ -42,35 +42,50 @@
    whose address is never taken (they cannot be modified through pointers). If
    the loop contains a function call, the condition [cond] should not contain
    global variables (as they may be modified in the function called).
-   A first analyze of the loop gathers all such variables modified within the
+   A first analysis of the loop gathers all such variables modified within the
    loop; all others are constant, and can be evaluated in the loop entry state.
 
    When computing the increment [v_delta] of a lvalue [v] in the loop, the
-   heuristic searches assignments "v = v ± i;". Any other assignment of [v]
-   cancels the heuristic. *)
+   heuristic searches assignments "v = v ± i;". Otherwise, if [v] is only
+   modified within the loop through an assignement "v = v2", the heuristic
+   computes the initial value and delta increment of variable [v2] instead.
+   This is required to deal with temporary variables introduced by the Frama-C
+   normalization.
+   Any other assignment of [v] cancels the heuristic. *)
 
 open Cil_types
 
-(* Is a statement a loop exit condition? If so, returns the condition and
-   whether the condition must hold to exit the loop. Otherwise, returns None. *)
-let is_conditional_break stmt =
-  match stmt.skind with
-  | If (cond, {bstmts=[{skind=Break _}]}, _, _) -> Some (cond, true)
-  | If (cond, _, {bstmts=[{skind=Break _}]}, _) -> Some (cond, false)
-  | _ -> None
+let is_true = function
+  | `True | `TrueReduced _ -> true
+  | _ -> false
 
-(* Returns a loop exit condition, as the conditional expression and whether
-   the condition must be zero or non-zero to exit the loop. *)
+(* Does a block exits a loop? *)
+let is_break block =
+  match block.bstmts with
+  | [{skind = Break _}] -> true
+  | _ -> false
+
+(* Returns a list of loop exit conditions. Each condition is expressed as an
+   expression and whether it must be zero or non-zero to exit the loop. *)
 let find_loop_exit_condition loop =
   let rec aux = function
-    | [] -> None
+    | [] -> []
     | stmt :: tl ->
-      match is_conditional_break stmt with
-      | Some _ as x -> x
-      | None -> aux tl
+      match stmt.skind with
+      | If (cond, b1, b2, _) when is_break b1 || is_break b2 ->
+        if is_break b1
+        then (cond, true) :: aux (b2.bstmts @ tl)
+        else (cond, false) :: aux (b1.bstmts @ tl)
+      | Block b -> aux (b.bstmts @ tl)
+      | _ -> aux tl
   in
   aux loop.bstmts
 
+let is_frama_c_builtin exp =
+  match exp.enode with
+  | Lval (Var vi, NoOffset) -> Ast_info.is_frama_c_builtin vi.vname
+  | _ -> false
+
 (* Effects of a loop:
    - set of varinfos that are directly modified within the loop. Pointer
      accesses are ignored.
@@ -105,7 +120,7 @@ let loop_effect_visitor = object (self)
     in
     let () = match instr with
       | Asm _ -> assembly <- true
-      | Call _ -> call <- true
+      | Call (_, exp, _, _) when not (is_frama_c_builtin exp) -> call <- true
       | _ -> ()
     in
     Cil.SkipChildren
@@ -143,7 +158,7 @@ let classify loop_effect lval =
       else
         (* If the address of the variable is taken, it could be modified within
            the loop. We suppose here that this is not the case, but this could
-           lead to some loop unrolling. *)
+           lead to some untimely loop unrolling. *)
         Constant
     | Mem _, _ -> Unsuitable (* Pointers are not supported by the heuristic. *)
   and is_const_offset = function
@@ -177,50 +192,48 @@ let find_lonely_candidate loop_effect expr =
   in
   aux None lvalues
 
-(* Returns true if the instruction assigns [lval]. *)
+(* Returns true if the instruction does not modify [lval]. *)
 let is_safe_instruction lval = function
   | Set (lv, _, _)
   | Call (Some lv, _, _, _) -> not (Cil_datatype.LvalStructEq.equal lval lv)
   | Call (None, _, _, _) | Local_init _ | Skip _ | Code_annot _ -> true
   | Asm _ -> false
 
-(* Returns true if the statement may assign [lval] during an iteration of the
-   loop [loop]. [lval] is a candidate for the automatic loop unroll heuristic,
-   and thus is modified within the loop. *)
-let is_safe lval ~loop stmt =
-  (* The current block being checked for a goto statement. *)
-  let current_block = ref None in
-  let rec is_safe_stmt stmt =
+(* Returns true if the statement [stmt] of function [kf] does not modify [lval].
+   [lval] is a candidate for the automatic loop unrolling of [loop] [loop]. *)
+let is_constant kf ~loop lval stmt =
+  let rec is_safe_stmt ~goto stmt =
     match stmt.skind with
     | Instr instr -> is_safe_instruction lval instr
     | Return _ | Break _ | Continue _ -> true
-    | If (_, b_then, b_else, _) -> is_safe_block b_then && is_safe_block b_else
+    | If (_, b_then, b_else, _) ->
+      is_safe_block ~goto b_then && is_safe_block ~goto b_else
     | Block b
     | Switch (_, b, _, _)
-    | Loop (_, b, _, _, _) -> is_safe_block b
+    | Loop (_, b, _, _, _) -> is_safe_block ~goto b
     | UnspecifiedSequence list ->
-      List.for_all (fun (stmt, _, _, _, _) -> is_safe_stmt stmt) list
-    | Goto (dest, _) -> begin
-        let dest_blocks = Kernel_function.find_all_enclosing_blocks !dest in
-        (* If the goto leaves the loop, then it is safe. *)
-        if List.mem loop dest_blocks then true else
-          (* If the goto moves into the block currently being checked, then it
-             is safe if the block is safe (which we are currently checking). *)
-          match !current_block with
-          | Some current_block when List.mem current_block dest_blocks -> true
-          | _ ->
-            (* Otherwise, we need to check that the whole block englobing
-               both the source and the destination of the goto is safe. *)
-            let block = Kernel_function.common_block !dest stmt in
-            current_block := Some block;
-            (* If this block is the loop itself, then it is not safe, as [lval]
-               is modified within the loop. *)
-            not (block = loop) && is_safe_block block
-      end
+      List.for_all (fun (stmt, _, _, _, _) -> is_safe_stmt ~goto stmt) list
+    | Goto (dest, _) ->
+      (* If [goto] holds, we are already checking a block for a [goto]. Do not
+         process goto statements again here. *)
+      goto ||
+      let first_stmt = List.hd loop.bstmts in
+      (* If the loop cannot be reached from [dest], then it is safe. *)
+      not (Stmts_graph.stmt_can_reach kf !dest first_stmt) ||
+      (* Otherwise, if the goto leaves the loop, then it forms another loop
+         that contains the current loop, which we don't want to unroll. *)
+      let dest_blocks = Kernel_function.find_all_enclosing_blocks !dest in
+      List.exists (Cil_datatype.Block.equal loop) dest_blocks &&
+      (* Otherwise, the goto stays within the loop: check that the block
+         englobing both the source and the destination is safe. *)
+      let block = Kernel_function.common_block !dest stmt in
+      (* If this block is the loop itself, then it is not safe,
+         as [lval] is modified within the loop. *)
+      not (block == loop) && is_safe_block ~goto:true block
     | _ -> false
   (* A block is safe if all its statements are safe. *)
-  and is_safe_block block = List.for_all is_safe_stmt block.bstmts in
-  is_safe_stmt stmt
+  and is_safe_block ~goto b = List.for_all (is_safe_stmt ~goto) b.bstmts in
+  is_safe_stmt ~goto:false stmt
 
 
 module Make (Abstract: Abstractions.Eva) = struct
@@ -262,9 +275,23 @@ module Make (Abstract: Abstractions.Eva) = struct
       (* If the new value of [expr] is top, no reduction has been performed. *)
       if Val.(equal top value) then None else Some (value, record)
     in
-    (* Different strategies whether cvalue is present. *)
-    match Val.get Main_values.CVal.key with
-    | Some get_cvalue ->
+    (* Assumes that [condition] is [positive]. Returns an over-approximation
+       of the values for which [condition] is [positive]. *)
+    reduce positive >>= fun (value, record) ->
+    (* Evaluates [condition] with the hypothesis [expr] ∈ [value], to check
+       whether [expr] ∈ [value] ⇒ [condition] = [positive]. *)
+    let valuation = Valuation.add valuation expr record in
+    fst (Eval.evaluate ~valuation ~reduction:false state condition)
+    >> fun (_valuation, v) ->
+    let satisfied =
+      if positive
+      then not Val.(is_included zero v)
+      else Val.(equal zero v)
+    in
+    (* If the condition is satisfied, returns [value]. Otherwise, uses a
+       specific feature to cvalue (if possible) to compute a better value. *)
+    if satisfied then Some value else
+      Val.get Main_values.CVal.key >>= fun get_cvalue ->
       (* Assumes that [condition] is NOT [positive]. *)
       reduce (not positive) >>= fun (value, _record) ->
       (* [value] is an over-approximation of the values of [expr] for which
@@ -273,21 +300,6 @@ module Make (Abstract: Abstractions.Eva) = struct
       let cvalue = get_cvalue value in
       cvalue_complement (Cil.typeOf expr) cvalue >>= fun cvalue ->
       Some (Val.set Main_values.CVal.key cvalue Val.top)
-    | None ->
-      (* Assumes that [condition] is [positive]. Returns an over-approximation
-         of the values for which [condition] is [positive]. *)
-      reduce positive >>= fun (value, record) ->
-      (* Evaluates [condition] with the hypothesis [expr] ∈ [value], to check
-         whether [expr] ∈ [value] ⇒ [condition] = [positive]. *)
-      let valuation = Valuation.add valuation expr record in
-      fst (Eval.evaluate ~valuation ~reduction:false state condition)
-      >> fun (_valuation, v) ->
-      let satisfied =
-        if positive
-        then not Val.(is_included zero v)
-        else Val.(equal zero v)
-      in
-      if satisfied then Some value else None
 
   (* Same as [reduce_to_expr] above, but builds the proper valuation from the
      [state]. [state] is the entry state of the loop, and [expr] is the only
@@ -379,7 +391,7 @@ module Make (Abstract: Abstractions.Eva) = struct
      should be a direct access to a variable whose address is not taken,
      and which should not be global if the loop contains function calls.
      Returns None if no increment can be computed. *)
-  let compute_delta lval loop =
+  let compute_delta kf lval loop =
     let rec delta_stmt acc stmt =
       match stmt.skind with
       | Instr instr -> delta_instruction lval acc instr
@@ -392,9 +404,11 @@ module Make (Abstract: Abstractions.Eva) = struct
       | If (_e, b1, b2, _loc) ->
         join_delta (delta_block acc b1) (delta_block acc b2)
       | Block b -> delta_block acc b
+      | UnspecifiedSequence list ->
+        List.fold_left (fun acc (s, _, _, _, _) -> delta_stmt acc s) acc list
       | _ ->
         (* For other statements, we only check that they do not modify [lval]. *)
-        if is_safe lval ~loop stmt then acc else raise NoIncrement
+        if is_constant kf ~loop lval stmt then acc else raise NoIncrement
     and delta_block acc block =
       List.fold_left delta_stmt acc block.bstmts
     in
@@ -404,6 +418,57 @@ module Make (Abstract: Abstractions.Eva) = struct
       final_delta delta >> fun d -> Some d
     with NoIncrement -> None
 
+  (* If in the block [loop], [lval] is assigned once to the value of another
+     lvalue, returns this new lvalue. Otherwise, returns [lval]. *)
+  let cross_equality lval loop =
+    (* If no such single equality can be found, return [lval] unchanged. *)
+    let exception No_equality in
+    let rec find_lval acc expr =
+      if acc <> None then raise No_equality else
+        match expr.enode with
+        | Lval lval -> Some lval
+        | Info (e, _) -> find_lval acc e
+        | _ -> raise No_equality
+    in
+    let cross_instr acc = function
+      | Set (lv, expr, _loc) when Cil_datatype.LvalStructEq.equal lv lval ->
+        find_lval acc expr
+      | Local_init (varinfo, AssignInit (SingleInit expr), _loc)
+        when Cil_datatype.LvalStructEq.equal (Cil.var varinfo) lval ->
+        find_lval acc expr
+      | Call (Some lv, _, _, _) when Cil_datatype.LvalStructEq.equal lval lv ->
+        raise No_equality
+      | _ -> acc
+    in
+    let rec cross_stmt acc stmt =
+      match stmt.skind with
+      | Instr instr -> cross_instr acc instr
+      | Block block -> cross_block acc block
+      | UnspecifiedSequence list ->
+        List.fold_left (fun acc (s, _, _, _, _) -> cross_stmt acc s) acc list
+      | If (_, {bstmts=[{skind=Break _}]}, block, _)
+      | If (_, block, {bstmts=[{skind=Break _}]}, _) -> cross_block acc block
+      | _ -> acc
+    and cross_block acc block =
+      List.fold_left cross_stmt acc block.bstmts
+    in
+    match cross_block None loop with
+    | None -> lval
+    | Some lval -> lval
+    | exception No_equality -> lval
+
+  (* If [lval] is a varinfo out-of-scope at statement [stmt] of function [kf],
+     introduces it to the [state]. *)
+  let enter_scope state kf stmt lval =
+    match lval with
+    | Var vi, _ when not (vi.vglob || vi.vformal
+                          || Kernel_function.var_is_in_scope stmt vi) ->
+      let kind = Abstract_domain.Local kf in
+      let state = Abstract.Dom.enter_scope kind [vi] state in
+      let location = Abstract.Loc.eval_varinfo vi in
+      Abstract.Dom.logic_assign None location state
+    | _ -> state
+
   (* Evaluates the lvalue [lval] in the state [state]. Returns None if the value
      may be undeterminate. *)
   let evaluate_lvalue state lval =
@@ -412,30 +477,55 @@ module Make (Abstract: Abstractions.Eva) = struct
     then None
     else flagged_value.v >> fun v -> Some v
 
+  let (>>:) v f = match v with Some v -> f v | None -> false
+
   (* Is the number of iterations of a loop bounded by [limit]?
      [state] is the loop entry state, and [loop_block] the block of the loop. *)
-  let is_bounded_loop state limit loop_block =
+  let is_bounded_loop kf stmt state limit loop_block =
     (* Computes the effect of the loop. Stops if it contains assembly code. *)
-    loop_effect_visitor#compute_effect loop_block >>= fun loop_effect ->
-    (* Finds the first loop exit condition, or stops. *)
-    find_loop_exit_condition loop_block >>= fun (condition, positive) ->
-    (* Finds the unique integer lvalue modified within the loop in [condition].
-       Stops if it does not exist is not a good candidate for the heuristic. *)
-    find_lonely_candidate loop_effect condition >>= fun lval ->
-    (* Reduce [condition] to a sufficient hypothesis over the [lval] value:
-       if [lval] ∈ [v_exit] then [condition = positive]. *)
-    reduce_to_lval_from_state state lval condition positive >>= fun v_exit ->
-    (* Evaluates the initial value [v_init] of [lval] in the loop entry state. *)
-    evaluate_lvalue state lval >>= fun v_init ->
-    (* Computes an over-approximation [v_delta] of the increment of [lval]
-       in one iteration of the loop. *)
-    compute_delta lval loop_block >>= fun v_delta ->
-    let typ = Cil.typeOfLval lval in
-    let limit = Val.inject_int typ (Integer.of_int limit) in
-    (* Checks whether [v_init] + [limit] × [v_delta] ⊂ [v_exit]. *)
-    let binop op v1 v2 = Bottom.non_bottom (Val.forward_binop typ op v1 v2) in
-    let value = binop PlusA v_init (binop Mult limit v_delta) in
-    Some (Val.is_included value v_exit)
+    loop_effect_visitor#compute_effect loop_block >>: fun loop_effect ->
+    (* Finds loop exit conditions. *)
+    let exit_conditions = find_loop_exit_condition loop_block in
+    (* Does the condition [condition = positive] limits the number of iterations
+       of the loop by [limit]? *)
+    let is_bounded_by_condition (condition, positive) =
+      (* Finds the unique integer lvalue modified within the loop in [condition].
+         Stops if it does not exist is not a good candidate for the heuristic. *)
+      find_lonely_candidate loop_effect condition >>: fun lval ->
+      (* If [lval] is not in scope at [stmt], introduces it into [state] so that
+         [lval] can be properly evaluated in [state]. *)
+      let state = enter_scope state kf stmt lval in
+      (* Reduce [condition] to a sufficient hypothesis over the [lval] value:
+         if [lval] ∈ [v_exit] then [condition = positive]. *)
+      reduce_to_lval_from_state state lval condition positive >>: fun v_exit ->
+      (* If [lval] is only assigned to the value of another lvalue, uses it
+         instead. This is especially useful to deal with temporary variables
+         introduced by the Frama-C normalization. *)
+      let lval = cross_equality lval loop_block in
+      (* Evaluates the initial value [v_init] of [lval] in the loop entry state. *)
+      evaluate_lvalue state lval >>: fun v_init ->
+      (* Computes an over-approximation [v_delta] of the increment of [lval]
+         in one iteration of the loop. *)
+      compute_delta kf lval loop_block >>: fun v_delta ->
+      let typ = Cil.typeOfLval lval in
+      let binop op v1 v2 = Bottom.non_bottom (Val.forward_binop typ op v1 v2) in
+      (* Possible iterations numbers to exit the loop. *)
+      let iter_nb = binop Div (binop MinusA v_exit v_init) v_delta in
+      let bound = Abstract_value.Int (Integer.of_int limit) in
+      (* Use the iteration number if it is always smaller than the [limit].
+         Otherwise use [limit]. *)
+      let limit =
+        if is_true (Val.assume_bounded Alarms.Upper_bound bound iter_nb)
+        then iter_nb
+        else Val.inject_int typ (Integer.of_int limit)
+      in
+      (* Checks whether [v_init] + [limit] × [v_delta] ⊂ [v_exit]. *)
+      let value = binop PlusA v_init (binop Mult limit v_delta) in
+      Val.is_included value v_exit
+    in
+    (* Tests whether at least one of the exit conditions limits the number of
+       iteration by [limit]. *)
+    List.exists is_bounded_by_condition exit_conditions
 
   (* Computes an automatic loop unrolling for statement [stmt] in state [state],
      with a maximum limit. Returns None for no automatic loop unrolling. *)
@@ -445,8 +535,9 @@ module Make (Abstract: Abstractions.Eva) = struct
       let loop_stmt = Kernel_function.find_enclosing_loop kf stmt in
       match loop_stmt.skind with
       | Loop (_code_annot, block, _loc, _, _) ->
-        is_bounded_loop state max_unroll block >>= fun bounded ->
-        if bounded then Some max_unroll else None
+        if is_bounded_loop kf stmt state max_unroll block
+        then Some max_unroll
+        else None
       | _ -> None
     with Not_found -> None
 end
diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
index d3a1a1ce141f3d23490482ee26cd1bd80b54995b..c713c76af25052cc62fbe9a6f24e02b9ab85a9cf 100644
--- a/tests/value/auto_loop_unroll.c
+++ b/tests/value/auto_loop_unroll.c
@@ -81,14 +81,6 @@ void various_loops () {
   }
   Frama_C_show_each_32_80(res);
   res = 0;
-  /* Other loop breaking condition. */
-  for (int i = 0; i < 111; i++) {
-    res++;
-    if (undet && res > 10)
-      break;
-  }
-  Frama_C_show_each_11_111(res);
-  res = 0;
   /* More complex loop condition. */
   int x = 24;
   int k = Frama_C_interval(0, 10);
@@ -96,6 +88,12 @@ void various_loops () {
     res++;
   Frama_C_show_each_40_50(res);
   res = 0;
+  /* Global loop counter. */
+  for (g = 0; g < 101; g++) {
+    res++;
+  }
+  Frama_C_show_each_101(res);
+  res = 0;
   /* Loop calling some functions that do not modify the loop counter. */
   for (int i = 0; i < 25; i++) {
     incr_g();
@@ -113,6 +111,16 @@ void various_loops () {
   }
   Frama_C_show_each_120(res);
   res = 0;
+  /* Loop counter modified on both sides of a conditional statement. */
+  for (int i = 0; i < 64;) {
+    if (undet)
+      i++;
+    else
+      i+=2;
+    res++;
+  }
+  Frama_C_show_each_32_64(res);
+  res = 0;
 }
 
 /* Loops that cannot be unrolled. */
@@ -120,8 +128,9 @@ void complex_loops () {
   /* Loop counter modified through a pointer. */
   int res = 0;
   int i = 0;
-  int *p = &i;
-  while (i < 64) {
+  int j = 0;
+  int *p = &j;
+  while (j < 64) {
     (*p)++;
     res++;
   }
@@ -147,17 +156,7 @@ void complex_loops () {
   }
   Frama_C_show_each_imprecise(res);
   res = 0;
-  i = 0;
-  while (i < 10) {
-    if (undet)
-      i++;
-    else
-      i++;
-    res++;
-  }
-  Frama_C_show_each_imprecise(res);
   /* Loop counter modified by a function. */
-  res = 0;
   g = 0;
   while (g < 64) {
     incr_g();
@@ -177,16 +176,124 @@ void complex_loops () {
   res = 0;
   /* Random loop condition. */
   i = 0;
-  while (i < 64 && undet) {
+  while (i < 64 || undet) {
     i++;
     res++;
   }
   Frama_C_show_each_imprecise(res);
 }
 
+/* Examples of loops with other exit conditions than simple comparisons.
+   All loops could be automatically unrolled on the second run, but should
+   not be unrolled on the first run. */
+void various_conditions () {
+  int i, res = 0;
+  /* Exit conditions using equality. */
+  for (i = 11; i; i--) {
+    res++;
+  }
+  Frama_C_show_each_11(res);
+  res = 0;
+  for (i = 0; i != 12; i++) {
+    res++;
+  }
+  Frama_C_show_each_12(res);
+  res = 0;
+  /* Loops with conjonction of exit conditions. */
+  for (int i = 13 ; i-- && undet; ) {
+    res ++;
+  }
+  Frama_C_show_each_0_13(res);
+  res = 0;
+  for (int i = 14 ; undet && i-- ; ) {
+    res ++;
+  }
+  Frama_C_show_each_0_14(res);
+  res = 0;
+  /* Loops with several exit conditions. */
+  for (int i = 0 ; undet ; i++) {
+    if (undet || i >= 15)
+      break;
+    res ++;
+  }
+  Frama_C_show_each_0_15(res);
+  res = 0;
+  for (int i = 0; i < 111; i++) {
+    res++;
+    if (undet && res > 10)
+      break;
+  }
+  Frama_C_show_each_11_111(res);
+  res = 0;
+}
+
+/* Examples of loops where temporary variables are introduced by Frama-C.
+   All loops could be automatically unrolled on the second run, but should
+   not be unrolled on the first run. */
+void temporary_variables () {
+  int i, res = 0;
+  for (i = 0; i++ < 20;) {
+    res++;
+  }
+  Frama_C_show_each_20(res);
+  res = 0;
+  for (i = 21; i--;) {
+    res++;
+  }
+  Frama_C_show_each_21(res);
+}
+
+/* Examples of loops with goto statements. */
+void loops_with_goto () {
+  int i, res = 0;
+  for (i = 0; i < 30; i++) {
+    res++;
+    if (undet)
+      goto middle;
+  }
+  Frama_C_show_each_30(res);
+  res = 0;
+ middle: ;
+  /* Should never be unrolled. */
+  for (i = 0; i < 31; i++) {
+    res++;
+    if (undet)
+      goto middle;
+  }
+  Frama_C_show_each_top(res);
+  res = 0;
+  /* Should be unrolled, and [res] should be precise. */
+  for (i = 0; i < 32; i++) {
+    res++;
+    if (undet)
+      goto L1;
+  L1:;
+  }
+  Frama_C_show_each_32(res);
+  res = 0;
+  /* Should be unrolled, but [res] should still be imprecise. */
+  for (i = 0; i < 33; i++) {
+  L2:res++;
+    if (undet)
+      goto L2;
+  }
+  Frama_C_show_each_33_inf(res);
+  res = 0;
+  /* Should never be unrolled. */
+  for (i = 0; i < 34; res++) {
+  L3:i++;
+    if (undet)
+      goto L3;
+  }
+  Frama_C_show_each_top(res);
+  res = 0;
+}
 
 void main () {
   simple_loops ();
   various_loops ();
   complex_loops ();
+  various_conditions ();
+  temporary_variables ();
+  loops_with_goto ();
 }
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
index 359bdb60f2fc65fdc7521795c3637c8ef6d68cbd..6f274e90fbf7abce23780edf92b50af50d198603 100644
--- a/tests/value/oracle/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle
@@ -6,7 +6,7 @@
   undet ∈ [--..--]
   g ∈ {0}
 [eva] computing for function simple_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:189.
+  Called from tests/value/auto_loop_unroll.c:293.
 [eva] tests/value/auto_loop_unroll.c:24: starting to merge loop iterations
 [eva:alarm] tests/value/auto_loop_unroll.c:25: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
@@ -27,7 +27,7 @@
 [eva] Recording results for simple_loops
 [eva] Done for function simple_loops
 [eva] computing for function various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:190.
+  Called from tests/value/auto_loop_unroll.c:294.
 [eva] tests/value/auto_loop_unroll.c:57: starting to merge loop iterations
 [eva:alarm] tests/value/auto_loop_unroll.c:58: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
@@ -45,164 +45,235 @@
   signed overflow. assert res + 1 ≤ 2147483647;
 [eva] tests/value/auto_loop_unroll.c:82: 
   Frama_C_show_each_32_80: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:85: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:86: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:90: 
-  Frama_C_show_each_11_111: [0..2147483647]
 [eva] computing for function Frama_C_interval <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:94.
+  Called from tests/value/auto_loop_unroll.c:86.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/auto_loop_unroll.c:94: 
+[eva] tests/value/auto_loop_unroll.c:86: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/auto_loop_unroll.c:95: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:96: Warning: 
+[eva] tests/value/auto_loop_unroll.c:87: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:88: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:97: 
+[eva] tests/value/auto_loop_unroll.c:89: 
   Frama_C_show_each_40_50: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:92: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:93: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:95: Frama_C_show_each_101: [0..2147483647]
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
-[eva] tests/value/auto_loop_unroll.c:100: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:98: starting to merge loop iterations
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:103.
+  Called from tests/value/auto_loop_unroll.c:101.
 [eva] Recording results for incr
 [eva] Done for function incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:100: Reusing old results for call to incr
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:103.
+  Called from tests/value/auto_loop_unroll.c:101.
 [eva] Recording results for incr
 [eva] Done for function incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva:alarm] tests/value/auto_loop_unroll.c:14: Warning: 
   signed overflow. assert g + 1 ≤ 2147483647;
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
-[eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:103.
-[eva] Recording results for incr
-[eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:100: Reusing old results for call to incr
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:103.
-[eva] Recording results for incr
-[eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
-[eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:103.
+  Called from tests/value/auto_loop_unroll.c:101.
 [eva:alarm] tests/value/auto_loop_unroll.c:18: Warning: 
   signed overflow. assert i + 1 ≤ 2147483647;
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: [0..2147483647]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:109: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:110: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:111: Warning: 
+[eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:108: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:107: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:108: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:109: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:112: Frama_C_show_each_120: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:115: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:120: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:122: 
+  Frama_C_show_each_32_64: [0..2147483647]
 [eva] Recording results for various_loops
 [eva] Done for function various_loops
 [eva] computing for function complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:191.
-[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:128: 
-  Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
+  Called from tests/value/auto_loop_unroll.c:295.
 [eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning: 
-  signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning: 
-  signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning: 
+[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:139: 
+[eva] tests/value/auto_loop_unroll.c:137: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:141: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:142: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:143: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
 [eva:alarm] tests/value/auto_loop_unroll.c:146: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:145: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
 [eva] tests/value/auto_loop_unroll.c:148: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning: 
+[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:155: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:158: 
+[eva] tests/value/auto_loop_unroll.c:157: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
 [eva] computing for function incr_g <- complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:163.
+  Called from tests/value/auto_loop_unroll.c:162.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
 [eva] computing for function incr_g <- complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:163.
+  Called from tests/value/auto_loop_unroll.c:162.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr_g <- complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:163.
+  Called from tests/value/auto_loop_unroll.c:162.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
-[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning: 
+[eva] computing for function incr_g <- complex_loops <- main.
+  Called from tests/value/auto_loop_unroll.c:162.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:167: 
+[eva] tests/value/auto_loop_unroll.c:166: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning: 
+[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:173: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:176: 
+[eva] tests/value/auto_loop_unroll.c:175: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning: 
+[eva] tests/value/auto_loop_unroll.c:179: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:181: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:184: 
+[eva:alarm] tests/value/auto_loop_unroll.c:180: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:183: 
   Frama_C_show_each_imprecise: [0..2147483647]
 [eva] Recording results for complex_loops
 [eva] Done for function complex_loops
+[eva] computing for function various_conditions <- main.
+  Called from tests/value/auto_loop_unroll.c:296.
+[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:193: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:197: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:198: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:203: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:203: Warning: 
+  signed overflow. assert -2147483648 ≤ i_0 - 1;
+[eva] tests/value/auto_loop_unroll.c:206: 
+  Frama_C_show_each_0_13: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:208: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:209: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:208: Warning: 
+  signed overflow. assert -2147483648 ≤ i_1 - 1;
+[eva] tests/value/auto_loop_unroll.c:211: 
+  Frama_C_show_each_0_14: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:214: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:217: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:219: 
+  Frama_C_show_each_0_15: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:221: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:222: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:226: 
+  Frama_C_show_each_11_111: [0..2147483647]
+[eva] Recording results for various_conditions
+[eva] Done for function various_conditions
+[eva] computing for function temporary_variables <- main.
+  Called from tests/value/auto_loop_unroll.c:297.
+[eva] tests/value/auto_loop_unroll.c:235: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:240: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: 
+  signed overflow. assert -2147483648 ≤ i - 1;
+[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
+[eva] Recording results for temporary_variables
+[eva] Done for function temporary_variables
+[eva] computing for function loops_with_goto <- main.
+  Called from tests/value/auto_loop_unroll.c:298.
+[eva] tests/value/auto_loop_unroll.c:249: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:250: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:259: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:263: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:266: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:276: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:275: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:280: 
+  Frama_C_show_each_33_inf: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:283: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:283: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_top: [0..2147483647]
+[eva] Recording results for loops_with_goto
+[eva] Done for function loops_with_goto
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -213,8 +284,9 @@
 [eva:final-states] Values at end of function complex_loops:
   g ∈ {64}
   res ∈ [0..2147483647]
-  i ∈ [0..64]
-  p ∈ {{ &i }}
+  i ∈ [64..2147483647]
+  j ∈ {64}
+  p ∈ {{ &j }}
   t[0] ∈ {0}
    [1] ∈ {1}
    [2] ∈ {2}
@@ -225,11 +297,20 @@
    [7] ∈ {7}
    [8] ∈ {8}
    [9] ∈ {9}
+[eva:final-states] Values at end of function loops_with_goto:
+  i ∈ [34..2147483647]
+  res ∈ {0}
 [eva:final-states] Values at end of function simple_loops:
   res ∈ {100}
+[eva:final-states] Values at end of function temporary_variables:
+  i ∈ [-2147483648..20]
+  res ∈ [0..2147483647]
+[eva:final-states] Values at end of function various_conditions:
+  i ∈ {12}
+  res ∈ {0}
 [eva:final-states] Values at end of function various_loops:
   Frama_C_entropy_source ∈ [--..--]
-  g ∈ [0..2147483647]
+  g ∈ [101..2147483647]
   res ∈ {0}
   x ∈ {24}
   k ∈ [0..10]
@@ -242,8 +323,14 @@
 [from] Done for function incr_g
 [from] Computing for function complex_loops
 [from] Done for function complex_loops
+[from] Computing for function loops_with_goto
+[from] Done for function loops_with_goto
 [from] Computing for function simple_loops
 [from] Done for function simple_loops
+[from] Computing for function temporary_variables
+[from] Done for function temporary_variables
+[from] Computing for function various_conditions
+[from] Done for function various_conditions
 [from] Computing for function various_loops
 [from] Computing for function Frama_C_interval <-various_loops
 [from] Done for function Frama_C_interval
@@ -261,11 +348,17 @@
   g FROM g
 [from] Function complex_loops:
   g FROM \nothing
+[from] Function loops_with_goto:
+  NO EFFECTS
 [from] Function simple_loops:
   NO EFFECTS
+[from] Function temporary_variables:
+  NO EFFECTS
+[from] Function various_conditions:
+  NO EFFECTS
 [from] Function various_loops:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-  g FROM g (and SELF)
+  g FROM \nothing
 [from] Function main:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   g FROM \nothing
@@ -279,16 +372,28 @@
 [inout] Inputs for function incr_g:
     g
 [inout] Out (internal) for function complex_loops:
-    g; res; i; p; j; t[0..9]
+    g; res; i; j; p; j_0; t[0..9]
 [inout] Inputs for function complex_loops:
     undet; g
+[inout] Out (internal) for function loops_with_goto:
+    i; res
+[inout] Inputs for function loops_with_goto:
+    undet
 [inout] Out (internal) for function simple_loops:
     res; i; i_0; i_1; i_2
 [inout] Inputs for function simple_loops:
     \nothing
+[inout] Out (internal) for function temporary_variables:
+    i; res; tmp; tmp_0
+[inout] Inputs for function temporary_variables:
+    \nothing
+[inout] Out (internal) for function various_conditions:
+    i; res; i_0; tmp; i_1; tmp_0; i_2; i_3
+[inout] Inputs for function various_conditions:
+    undet
 [inout] Out (internal) for function various_loops:
-    Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5; 
-    t; i_6; j
+    Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; x; k; i_3; i_4; t; 
+    i_5; j; i_6
 [inout] Inputs for function various_loops:
     Frama_C_entropy_source; undet; g
 [inout] Out (internal) for function main:
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 775a7323bf9b696e565c5de92ee3cf0bbbcbeda7..f743d1ef27eb2cd2660b39dfd87b47cfe3c26d19 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -6,7 +6,7 @@
   undet ∈ [--..--]
   g ∈ {0}
 [eva] computing for function simple_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:189.
+  Called from tests/value/auto_loop_unroll.c:293.
 [eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling.
 [eva] tests/value/auto_loop_unroll.c:24: 
   Trace partitioning superposing up to 100 states
@@ -25,7 +25,7 @@
 [eva] Recording results for simple_loops
 [eva] Done for function simple_loops
 [eva] computing for function various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:190.
+  Called from tests/value/auto_loop_unroll.c:294.
 [eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling.
 [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
 [eva:loop-unroll] tests/value/auto_loop_unroll.c:62: Automatic loop unrolling.
@@ -36,319 +36,376 @@
 [eva] tests/value/auto_loop_unroll.c:75: 
   Trace partitioning superposing up to 100 states
 [eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..80]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:85: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:90: Frama_C_show_each_11_111: [11..111]
 [eva] computing for function Frama_C_interval <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:94.
+  Called from tests/value/auto_loop_unroll.c:86.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/auto_loop_unroll.c:94: 
+[eva] tests/value/auto_loop_unroll.c:86: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:95: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:97: Frama_C_show_each_40_50: [40..50]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:100: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:87: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:89: Frama_C_show_each_40_50: [40..50]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:92: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:95: Frama_C_show_each_101: {101}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:98: Automatic loop unrolling.
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 [eva] computing for function incr_g <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:101.
+  Called from tests/value/auto_loop_unroll.c:99.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr <- various_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:102.
+  Called from tests/value/auto_loop_unroll.c:100.
 [eva] Recording results for incr
 [eva] Done for function incr
-[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
-[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: {25}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:109: Automatic loop unrolling.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: {120}
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: {25}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:107: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:108: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:112: Frama_C_show_each_120: {120}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:115: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..64]
 [eva] Recording results for various_loops
 [eva] Done for function various_loops
 [eva] computing for function complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:191.
-[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:128: 
-  Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
+  Called from tests/value/auto_loop_unroll.c:295.
 [eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning: 
-  signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning: 
-  signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning: 
+[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:139: 
+[eva] tests/value/auto_loop_unroll.c:137: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:141: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:142: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:143: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
 [eva:alarm] tests/value/auto_loop_unroll.c:146: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:145: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
 [eva] tests/value/auto_loop_unroll.c:148: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning: 
+[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:155: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:158: 
+[eva] tests/value/auto_loop_unroll.c:157: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
 [eva] computing for function incr_g <- complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:163.
+  Called from tests/value/auto_loop_unroll.c:162.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
 [eva] computing for function incr_g <- complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:163.
+  Called from tests/value/auto_loop_unroll.c:162.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
 [eva] computing for function incr_g <- complex_loops <- main.
-  Called from tests/value/auto_loop_unroll.c:163.
+  Called from tests/value/auto_loop_unroll.c:162.
 [eva] Recording results for incr_g
 [eva] Done for function incr_g
-[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
-[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
-[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning: 
+[eva] computing for function incr_g <- complex_loops <- main.
+  Called from tests/value/auto_loop_unroll.c:162.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:167: 
+[eva] tests/value/auto_loop_unroll.c:166: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning: 
+[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:173: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:176: 
+[eva] tests/value/auto_loop_unroll.c:175: 
   Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning: 
+[eva] tests/value/auto_loop_unroll.c:179: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:181: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:184: 
+[eva:alarm] tests/value/auto_loop_unroll.c:180: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:183: 
   Frama_C_show_each_imprecise: [0..2147483647]
 [eva] Recording results for complex_loops
 [eva] Done for function complex_loops
+[eva] computing for function various_conditions <- main.
+  Called from tests/value/auto_loop_unroll.c:296.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:192: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:197: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:203: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_0_13: [0..13]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:208: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:211: Frama_C_show_each_0_14: [0..14]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:214: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_0_15: [0..15]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:221: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:221: 
+  Trace partitioning superposing up to 100 states
+[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11_111: [11..111]
+[eva] Recording results for various_conditions
+[eva] Done for function various_conditions
+[eva] computing for function temporary_variables <- main.
+  Called from tests/value/auto_loop_unroll.c:297.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:235: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: {20}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
+[eva] Recording results for temporary_variables
+[eva] Done for function temporary_variables
+[eva] computing for function loops_with_goto <- main.
+  Called from tests/value/auto_loop_unroll.c:298.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:249: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: {30}
+[eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:259: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:263: Frama_C_show_each_top: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:266: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: {32}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:275: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:276: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:276: 
+  Trace partitioning superposing up to 100 states
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:278: 
+  loop not completely unrolled
+[eva:alarm] tests/value/auto_loop_unroll.c:276: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:280: 
+  Frama_C_show_each_33_inf: [33..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning: 
+  signed overflow. assert i + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:283: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:283: Warning: 
+  signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:288: Frama_C_show_each_top: [0..2147483647]
+[eva] Recording results for loops_with_goto
+[eva] Done for function loops_with_goto
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function incr:
   __retres ∈ [1..25]
 [eva:final-states] Values at end of function incr_g:
-  g ∈ [1..63]
+  g ∈ [1..126]
 [eva:final-states] Values at end of function complex_loops:
   g ∈ {64}
   res ∈ [0..2147483647]
-  i ∈ [0..64]
-  p ∈ {{ &i }}
+  i ∈ [64..2147483647]
+  j ∈ {64}
+  p ∈ {{ &j }}
   t[0] ∈ {0}
    [1] ∈ {1}
    [2] ∈ {2}
@@ -359,11 +416,20 @@
    [7] ∈ {7}
    [8] ∈ {8}
    [9] ∈ {9}
+[eva:final-states] Values at end of function loops_with_goto:
+  i ∈ [34..2147483647]
+  res ∈ {0}
 [eva:final-states] Values at end of function simple_loops:
   res ∈ {100}
+[eva:final-states] Values at end of function temporary_variables:
+  i ∈ {-1}
+  res ∈ {21}
+[eva:final-states] Values at end of function various_conditions:
+  i ∈ {12}
+  res ∈ {0}
 [eva:final-states] Values at end of function various_loops:
   Frama_C_entropy_source ∈ [--..--]
-  g ∈ {25}
+  g ∈ {126}
   res ∈ {0}
   x ∈ {24}
   k ∈ [0..10]
@@ -376,8 +442,14 @@
 [from] Done for function incr_g
 [from] Computing for function complex_loops
 [from] Done for function complex_loops
+[from] Computing for function loops_with_goto
+[from] Done for function loops_with_goto
 [from] Computing for function simple_loops
 [from] Done for function simple_loops
+[from] Computing for function temporary_variables
+[from] Done for function temporary_variables
+[from] Computing for function various_conditions
+[from] Done for function various_conditions
 [from] Computing for function various_loops
 [from] Computing for function Frama_C_interval <-various_loops
 [from] Done for function Frama_C_interval
@@ -395,11 +467,17 @@
   g FROM g
 [from] Function complex_loops:
   g FROM \nothing
+[from] Function loops_with_goto:
+  NO EFFECTS
 [from] Function simple_loops:
   NO EFFECTS
+[from] Function temporary_variables:
+  NO EFFECTS
+[from] Function various_conditions:
+  NO EFFECTS
 [from] Function various_loops:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-  g FROM g (and SELF)
+  g FROM \nothing
 [from] Function main:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   g FROM \nothing
@@ -413,16 +491,28 @@
 [inout] Inputs for function incr_g:
     g
 [inout] Out (internal) for function complex_loops:
-    g; res; i; p; j; t[0..9]
+    g; res; i; j; p; j_0; t[0..9]
 [inout] Inputs for function complex_loops:
     undet; g
+[inout] Out (internal) for function loops_with_goto:
+    i; res
+[inout] Inputs for function loops_with_goto:
+    undet
 [inout] Out (internal) for function simple_loops:
     res; i; i_0; i_1; i_2
 [inout] Inputs for function simple_loops:
     \nothing
+[inout] Out (internal) for function temporary_variables:
+    i; res; tmp; tmp_0
+[inout] Inputs for function temporary_variables:
+    \nothing
+[inout] Out (internal) for function various_conditions:
+    i; res; i_0; tmp; i_1; tmp_0; i_2; i_3
+[inout] Inputs for function various_conditions:
+    undet
 [inout] Out (internal) for function various_loops:
-    Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5; 
-    t; i_6; j
+    Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; x; k; i_3; i_4; t; 
+    i_5; j; i_6
 [inout] Inputs for function various_loops:
     Frama_C_entropy_source; undet; g
 [inout] Out (internal) for function main: