diff --git a/offline_tests/test.ml b/offline_tests/test.ml
index 3bf5d032020e5ab1fcac0115ada651fb9c9591dc..9cd95f0b06bc39bdaa03ffcf608aeaf4559627b2 100644
--- a/offline_tests/test.ml
+++ b/offline_tests/test.ml
@@ -270,7 +270,9 @@ let print_results ok ko w n =
 
 let lustrec_params f =
   let ps = [ "-acsl-spec"; "-d"; dir; f ] in
-  Option.fold ~none:ps ~some:(fun x -> "-O" :: string_of_int x :: ps)
+  Option.fold
+    ~none:ps
+    ~some:(fun x -> "-O" :: string_of_int x :: ps)
     optimization_level
 
 let compile report lustrec fs =
@@ -302,8 +304,8 @@ let compile report lustrec fs =
           if is_compiled report f then success report
           else if is_ninit report f then ninit report
           else
-            let cmd = Filename.quote_command ~stderr:err_f lustrec
-              (lustrec_params f)
+            let cmd =
+              Filename.quote_command ~stderr:err_f lustrec (lustrec_params f)
             in
             let ic = open_process_in cmd in
             let b =
@@ -352,11 +354,10 @@ let wp_args =
 let wp_module = "strategy.ml"
 
 let wp_strategy =
-  String.concat ","
+  String.concat
+    ","
     [
-      "LustreC:Transitions";
-      (* "LustreC:ResetCleared"; *)
-      "LustreC:MemoryPacks"
+      "LustreC:Transitions"; (* "LustreC:ResetCleared"; *) "LustreC:MemoryPacks";
     ]
 
 let wp_auto_depth = 100 |> string_of_int
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index 1241e9725d383607103b095c51e6ad85cc126437..e681a94b922ea8b2dfac6af02e062dc45299cf93 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -111,11 +111,11 @@ let rec pp_machine_instr typed_submachines env instr fmt =
       @ if output != [] then [ output ] else []
     in
     pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
-  | MBranch (_, []) ->
+  | MBranch (_, [], _) ->
     assert false
-  | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
+  | MBranch (g, (c1, i1) :: tl, _) when c1 = tag_false || c1 = tag_true ->
     pp_if fmt (build_if g c1 i1 tl)
-  | MBranch (g, hl) ->
+  | MBranch (g, hl, _) ->
     pp_case fmt (g, hl)
   | MComment s ->
     let lines = String.split_on_char '\n' s in
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index c321b6732270ecc7d47082c7c596045afb198a01..bb8d54885d826bdb7ba36269f46cf0219ee44e3c 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -59,7 +59,7 @@ let rec find_submachine_step_call ident instr_list =
         ( List.map (function x -> x.value_type) vl,
           List.map (function x -> x.var_type) il );
       ]
-    | MBranch (_, l) ->
+    | MBranch (_, l, _) ->
       List.flatten
         (List.map (function _, y -> find_submachine_step_call ident y) l)
     | _ ->
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 92134e63524be7c31198c4eed08dd667aa289e4e..6aa2d1a3876f1d4c568df07fd7e2ef0adc056192 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -307,8 +307,10 @@ struct
 
   let pp_alloc_header header_fmt basename machines dependencies =
     (* Include once: start *)
-    let machines' = List.filter (fun m ->
-        not m.mis_contract && not (fst (get_stateless_status m)) ) machines
+    let machines' =
+      List.filter
+        (fun m -> (not m.mis_contract) && not (fst (get_stateless_status m)))
+        machines
     in
     let baseNAME = file_to_module_name basename in
     let self_dep =
@@ -454,7 +456,9 @@ struct
          ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
          pp_machine_struct_top_decl_from_header
          ~pp_epilogue:pp_print_cutcut)
-      (List.filter (fun td -> not (fst (get_stateless_status_top_decl td))) nodes)
+      (List.filter
+         (fun td -> not (fst (get_stateless_status_top_decl td)))
+         nodes)
       (* Print the prototypes of all machines *)
       (pp_print_list
          ~pp_open_box:pp_open_vbox0
@@ -466,8 +470,10 @@ struct
 
   let pp_memory_header header_fmt basename machines dependencies =
     (* Include once: start *)
-    let machines' = List.filter (fun m ->
-        not m.mis_contract && not (fst (get_stateless_status m)) ) machines
+    let machines' =
+      List.filter
+        (fun m -> (not m.mis_contract) && not (fst (get_stateless_status m)))
+        machines
     in
     let baseNAME = file_to_module_name basename in
     fprintf
@@ -505,8 +511,8 @@ struct
         pp
         ~pp_epilogue:pp_print_cutcut
     in
-    let machines' = List.filter (fun m -> not (fst (get_stateless_status m)))
-        machines
+    let machines' =
+      List.filter (fun m -> not (fst (get_stateless_status m))) machines
     in
     fprintf
       header_fmt
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index d02de9f4916ff54cdb77b14cebb7836d8f1da207..e05efb0679e069d856beeaad5a801e1e3ee00606 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1075,8 +1075,8 @@ module HdrMod = struct
         pp
         ~pp_epilogue:pp_print_cutcut
     in
-    let machines' = List.filter (fun m -> not (fst (get_stateless_status m)))
-        machines
+    let machines' =
+      List.filter (fun m -> not (fst (get_stateless_status m))) machines
     in
     fprintf
       fmt
@@ -1565,7 +1565,7 @@ module SrcMod = struct
           instr.instr_spec
       in
       match instr.instr_desc with
-      | MBranch (_, hl) ->
+      | MBranch (_, hl, _) ->
         List.fold_left (fun vs (_, il) -> List.fold_left gather vs il) vs hl
       | _ ->
         vs
@@ -1970,10 +1970,11 @@ let rec sanitize_instr i =
       MStateAssign (x, sanitize_value v)
     | MStep (xs, f, vs) ->
       MStep (sanitize_var_decls xs, f, sanitize_values vs)
-    | MBranch (v, brs) ->
+    | MBranch (v, brs, e) ->
       MBranch
         ( sanitize_value v,
-          List.map (fun (t, instrs) -> t, sanitize_instrs instrs) brs )
+          List.map (fun (t, instrs) -> t, sanitize_instrs instrs) brs,
+          e )
     | i ->
       i
   in
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index e47d137428bac9f9d243be256babdced413eb32c..7e3267f4cd92aff576f623ed76b12ef726fd1704 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -371,13 +371,13 @@ module Main (Mod : MODIFIERS_SRC) = struct
           pp_arrow_call m self mem fmt i il
         | _ ->
           pp_basic_instance_call m self mem fmt i vl il)
-      | MBranch (_, []) ->
+      | MBranch (_, [], _) ->
         eprintf
           "internal error: C_backend_src.pp_machine_instr %a@."
           (pp_instr m)
           instr;
         assert false
-      | MBranch (g, hl) ->
+      | MBranch (g, hl, e) ->
         if
           let t = fst (List.hd hl) in
           t = tag_true || t = tag_false
@@ -419,6 +419,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
                   m
                   self
                   mem
+                  e
                   (List.length hl)))
             hl
       | MSpec s ->
@@ -435,11 +436,11 @@ module Main (Mod : MODIFIERS_SRC) = struct
       else pp_print_nothing)
       instr
 
-  and pp_machine_branch ?(with_spec = true) dependencies m self mem n fmt i
+  and pp_machine_branch ?(with_spec = true) dependencies m self mem e n fmt i
       (t, h) =
     fprintf
       fmt
-      (if n > 1 && i = n - 1 then "@[<v 2>default: // %a@,%a@]"
+      (if e && i = n - 1 then "@[<v 2>default: // %a@,%a@]"
       else "@[<v 2>case %a:@,%a@,break;@]")
       pp_c_tag
       t
@@ -755,7 +756,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
         [
           mk_branch
             (mk_val ResetFlag Type_predef.type_bool)
-            [ "true", mkinstr (MResetAssign false) :: m.minit ];
+            [ "true", mkinstr (MResetAssign false) :: m.minit ]
+            false;
         ]
       fmt
 
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index d1eef9e4a55665e1c47851f0385faccf524eb792..e8b04b07c6c40f83a01a02dda75389d327d23836 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -225,7 +225,7 @@ and branch_instr_vars m i =
           in
           VSet.add reset_var args_vars
         else args_vars )
-  | MBranch (g, (_, hd_il) :: tl) ->
+  | MBranch (g, (_, hd_il) :: tl, _) ->
       (* We focus on variables defined in all branches *)
       let read_guard = get_expr_vars g in
       (* Bootstrapping with first item *)
@@ -313,7 +313,7 @@ let rec pp_emf_instr m fmt i =
           (reset_name id)
     (* TODO: handle clear_reset and reset flag *)
     | MClearReset | MResetAssign _ -> ()
-    | MBranch (g, hl) ->
+    | MBranch (g, hl, _) ->
         let all_outputs, outputs, inputs = branch_instr_vars m i in
 
         (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 1fa5c20686639a6248fc7ecca68a61af48406066..fcf0a0c6bd47e70ace8368acc3dc4d1569a26adb 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -380,7 +380,7 @@ let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr :
     reset_instances
   (* Since this instance call will only happen once, we don't have to update
      reset_instances *)
-  | MBranch (g, hl) ->
+  | MBranch (g, hl, _) ->
     (* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
        yet. Later, we will have to compare the reset_instances of each branch
        and introduced the mem_m = mem_c for branches to do not address it while
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 6338fbc4b753bae5da1b4d5dbd9d1c6f3b3857e8..0189f975eb20cc4e55fcbc2dccaddb3002cb4866 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -160,7 +160,7 @@ let rec translate_act env (y, expr) =
         hl
         ([], [])
     in
-    mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl
+    mk_branch' ~lustre_eq var_x hl true, mk_branch_tr var_x spec_hl
   | _ ->
     let e = translate_expr expr in
     mk_assign ~lustre_eq y e, mk_assign_tr y e
@@ -223,7 +223,8 @@ let ctx_init =
    building *)
 (****************************************************************)
 
-let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ]))
+let mk_control v l inst =
+  mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ], false))
 
 let control_on_clock env ck inst =
   let rec aux ((fspec, inst) as acc) ck =
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 4da14354099a1c63d6612a08e4a7aee65496d7c3..442d25285ea1dce581f7ca906aa40d2515f60258 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -206,7 +206,7 @@ let rec pp_instr m fmt i =
       i
       (pp_print_parenthesized pp_val)
       vl
-  | MBranch (g, hl) ->
+  | MBranch (g, hl, _) ->
     fprintf
       fmt
       "@[<v 2>case(%a) {@,%a@]@,}"
@@ -421,10 +421,10 @@ let id_to_tag id =
   mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
 
 let mk_conditional ?lustre_eq c t e =
-  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
+  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ], true))
 
-let mk_branch ?lustre_eq c br =
-  mkinstr ?lustre_eq (MBranch (c, sort_handlers br))
+let mk_branch ?lustre_eq c br e =
+  mkinstr ?lustre_eq (MBranch (c, sort_handlers br, e))
 
 let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
 let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
@@ -673,14 +673,15 @@ let rec join_branches hl1 hl2 =
 
 and join_guards inst1 insts2 =
   match get_instr_desc inst1, insts2 with
-  | ( MBranch (x1, hl1),
-      ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 )
+  | ( MBranch (x1, hl1, e1),
+      ({ instr_desc = MBranch (x2, hl2, e2); _ } as inst2) :: insts2 )
     when x1 = x2 ->
     mkinstr
       ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
       (* TODO on pourrait uniquement concatener les lustres de inst1 et
          hd(inst2) *)
-      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
+      (MBranch
+         (x1, join_branches (sort_handlers hl1) (sort_handlers hl2), e1 || e2))
     :: insts2
   | _ ->
     inst1 :: insts2
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 84a7e4aed6b74297f294512b6f9af41433b94708..b8598d0e361a680ef8f15c293ffaafecadd8a99a 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -22,10 +22,10 @@ val mk_conditional :
   ?lustre_eq:eq -> value_t -> instr_t list -> instr_t list -> instr_t
 
 val mk_branch :
-  ?lustre_eq:eq -> value_t -> (label * instr_t list) list -> instr_t
+  ?lustre_eq:eq -> value_t -> (label * instr_t list) list -> bool -> instr_t
 
 val mk_branch' :
-  ?lustre_eq:eq -> var_decl -> (label * instr_t list) list -> instr_t
+  ?lustre_eq:eq -> var_decl -> (label * instr_t list) list -> bool -> instr_t
 
 val mk_assign : ?lustre_eq:eq -> var_decl -> value_t -> instr_t
 val empty_machine : machine_t
diff --git a/src/machine_code_dep.ml b/src/machine_code_dep.ml
index 5e14a0f8fa1cf9442083c4b640af633500845fe3..ec7e1355764f8ea33c8fd6adbff60744f924c6a6 100644
--- a/src/machine_code_dep.ml
+++ b/src/machine_code_dep.ml
@@ -31,7 +31,7 @@ let rec add_instr_dependencies g deps instr =
     List.iter (add_expr_dependencies g i) deps
   | MSetReset i | MNoReset i ->
     List.iter (add_expr_dependencies g i) deps
-  | MBranch (e, hl) ->
+  | MBranch (e, hl, _) ->
     List.iter
       (fun (_, l) -> List.iter (add_instr_dependencies g (e :: deps)) l)
       hl
diff --git a/src/machine_code_types.mli b/src/machine_code_types.mli
index eff5d73d685140f877db566e3600f73bb5f68e84..106ae659ff0b60ea78049265ddfe8ba27f73dbe3 100644
--- a/src/machine_code_types.mli
+++ b/src/machine_code_types.mli
@@ -39,7 +39,7 @@ and instr_t_desc =
   | MSetReset of ident
   | MNoReset of ident
   | MStep of var_decl list * ident * value_t list
-  | MBranch of value_t * (label * instr_t list) list
+  | MBranch of value_t * (label * instr_t list) list * bool
   | MComment of string
   | MSpec of string
 
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index d0adaa3677959c5a17cbce9f886e06c7e059d598..e38cfc7f0e3de0c01775dbe47a7a8d0c89653539 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -158,12 +158,13 @@ let rec eliminate m elim instr =
     instr
   | MStep (il, i, vl) ->
     update_instr_desc instr (MStep (il, i, List.map e_val vl))
-  | MBranch (g, hl) ->
+  | MBranch (g, hl, e) ->
     update_instr_desc
       instr
       (MBranch
          ( e_val g,
-           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
+           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl,
+           e ))
 
 let rec fv_value m s v =
   match v.value_desc with
@@ -320,12 +321,13 @@ let rec simplify_instr_offset m instr =
     update_instr_desc
       instr
       (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
-  | MBranch (cond, brl) ->
+  | MBranch (cond, brl, e) ->
     update_instr_desc
       instr
       (MBranch
          ( simplify_expr_offset m cond,
-           List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl ))
+           List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl,
+           e ))
 
 and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs
 
@@ -432,7 +434,7 @@ let instrs_unfold m fanin elim instrs =
           ([ v.var_id ], (desome instr.lustre_eq).eq_rhs)
       in
       IMap.add v.var_id ((v, expr, new_eq), true) elim, instr :: instrs
-    | MBranch (g, hl) ->
+    | MBranch (g, hl, e) ->
       let elim, hl =
         List.fold_left
           (fun (elim', hl) (h, l) ->
@@ -441,7 +443,7 @@ let instrs_unfold m fanin elim instrs =
           (elim, [])
           hl
       in
-      elim, update_instr_desc instr (MBranch (g, List.rev hl)) :: instrs
+      elim, update_instr_desc instr (MBranch (g, List.rev hl, e)) :: instrs
     | _ ->
       elim, instr :: instrs
   in
@@ -472,14 +474,16 @@ let instrs_unfold m fanin elim instrs =
                IMap.mem v.var_id elim ->
           (* we transform the assignment into a comment in order to keep its
              spec *)
-          { instr with
+          {
+            instr with
             instr_spec = add_ghost_assign_spec v e instr.instr_spec;
-            instr_desc = assign_comment m v e }
-        | MBranch (g, hl) ->
+            instr_desc = assign_comment m v e;
+          }
+        | MBranch (g, hl, e) ->
           let instr =
             update_instr_desc
               instr
-              (MBranch (g, List.map (fun (h, l) -> h, filter l) hl))
+              (MBranch (g, List.map (fun (h, l) -> h, filter l) hl, e))
           in
           eliminate m elim_exprs instr
         | _ ->
@@ -628,7 +632,7 @@ let rec assigns_instr instr assign =
     VSet.add i assign
   | MStep (ol, _, _) ->
     List.fold_right VSet.add ol assign
-  | MBranch (_, hl) ->
+  | MBranch (_, hl, _) ->
     List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
   | _ ->
     assign
@@ -773,7 +777,7 @@ let rec instr_is_skip instr =
     true
   | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
     true
-  | MBranch (_, hl) ->
+  | MBranch (_, hl, _) ->
     List.for_all (fun (_, il) -> instrs_are_skip il) hl
   | _ ->
     false
@@ -869,19 +873,19 @@ let rec instr_replace_var m fvar instrs instr =
     | MStep (il, i, vl) ->
       let il = List.map fvar il in
       MStep (il, i, List.map (value_replace_var fvar) vl)
-    | MBranch (g, hl) ->
+    | MBranch (g, hl, e) ->
       let hl =
         List.fold_left
           (fun hl (h, il) ->
             let il = instrs_replace_var m fvar il in
             (* Format.(printf "%s: before %a after %a@." h (IMap.pp
                pp_print_int) asg (IMap.pp pp_print_int) asg''); *)
-            (h, il) :: hl )
+            (h, il) :: hl)
           []
           hl
       in
       (* Format.(printf "%a@." (IMap.pp pp_print_int) asg); *)
-      MBranch (value_replace_var fvar g, List.rev hl)
+      MBranch (value_replace_var fvar g, List.rev hl, e)
     | MSetReset _
     | MNoReset _
     | MClearReset
@@ -893,88 +897,106 @@ let rec instr_replace_var m fvar instrs instr =
   instr_cons { instr with instr_desc } instrs
 
 and instrs_replace_var m fvar instrs =
-  let instrs =
-    List.fold_left (instr_replace_var m fvar) [] instrs
-  in
+  let instrs = List.fold_left (instr_replace_var m fvar) [] instrs in
   List.rev instrs
 
 let add_ghost_assigns reuse instrs =
   let is_reused_def v = Hashtbl.find_opt reuse v.var_id in
   let add_reused vars i =
-    match is_reused_def i with
-    | None -> vars
-    | Some v -> VMap.add i v vars
+    match is_reused_def i with None -> vars | Some v -> VMap.add i v vars
   in
   let rec is_defining_reused vars instr =
     match instr.instr_desc with
-    | MLocalAssign (i, _) -> add_reused vars i
+    | MLocalAssign (i, _) ->
+      add_reused vars i
     | MStep (il, _, _) ->
       List.fold_left add_reused vars il
-    | MBranch (_, hl) ->
-      List.fold_left (fun vars (_, instrs) ->
-          List.fold_left is_defining_reused vars instrs)
-          vars hl
-    | _ -> vars
+    | MBranch (_, hl, _) ->
+      List.fold_left
+        (fun vars (_, instrs) -> List.fold_left is_defining_reused vars instrs)
+        vars
+        hl
+    | _ ->
+      vars
   in
-  List.map (fun instr ->
+  List.map
+    (fun instr ->
       let vars = is_defining_reused VMap.empty instr in
-      let instr_spec = VMap.fold (fun i v ->
-          add_ghost_assign_spec i (vdecl_to_val v))
-          vars instr.instr_spec
+      let instr_spec =
+        VMap.fold
+          (fun i v -> add_ghost_assign_spec i (vdecl_to_val v))
+          vars
+          instr.instr_spec
       in
-      { instr with instr_spec }) instrs
+      { instr with instr_spec })
+    instrs
 
 let ghost_vd v = { v with var_id = "__" ^ v.var_id }
 
 let add_ghost_assigns_reassigned rasg instrs =
   let _, instrs, _ =
-    List.fold_left (fun (rasg, instrs, fvar) instr ->
-      let rec aux rasg instr fvar =
-        match instr.instr_desc with
-        | MLocalAssign (i, _) when VSet.mem i rasg ->
-          VSet.remove i rasg,
-          add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) instr.instr_spec,
-          fun v -> if v = i then ghost_vd i else fvar v
-        | MStep (il, _, _) ->
-          let il = List.filter (fun i -> VSet.mem i rasg) il in
-          List.fold_left (fun (rasg, spec, fvar) i ->
-              VSet.remove i rasg,
-              add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec,
-              fun v -> if v = i then ghost_vd i else fvar v)
-            (rasg, instr.instr_spec, fvar) il
-        | MBranch (_, hl) ->
-          let rasg' = List.fold_left (fun rasg (_, instrs) ->
-              List.fold_left (fun rasg instr ->
-                  let rasg, _, _ = aux rasg instr fvar in
-                   rasg) rasg instrs) rasg hl
-          in
-          let rasg'' = VSet.diff rasg rasg' in
-          rasg',
-          VSet.fold (fun i spec ->
-              add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec)
-            rasg''
-            instr.instr_spec,
-          fun v -> if VSet.mem v rasg'' then ghost_vd v else fvar v
-        | _ -> rasg, instr.instr_spec, fvar
-      in
-      let rasg, instr_spec, fvar = aux rasg instr fvar in
-      let instr_spec = List.map (fun (t, b) ->
-          instr_spec_replace fvar t, b) instr_spec
-      in
-      rasg,
-      { instr with instr_spec } :: instrs,
-      fvar)
-    (rasg, [], fun v -> v) instrs
+    List.fold_left
+      (fun (rasg, instrs, fvar) instr ->
+        let rec aux rasg instr fvar =
+          match instr.instr_desc with
+          | MLocalAssign (i, _) when VSet.mem i rasg ->
+            ( VSet.remove i rasg,
+              add_ghost_assign_spec
+                (ghost_vd i)
+                (vdecl_to_val i)
+                instr.instr_spec,
+              fun v -> if v = i then ghost_vd i else fvar v )
+          | MStep (il, _, _) ->
+            let il = List.filter (fun i -> VSet.mem i rasg) il in
+            List.fold_left
+              (fun (rasg, spec, fvar) i ->
+                ( VSet.remove i rasg,
+                  add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec,
+                  fun v -> if v = i then ghost_vd i else fvar v ))
+              (rasg, instr.instr_spec, fvar)
+              il
+          | MBranch (_, hl, _) ->
+            let rasg' =
+              List.fold_left
+                (fun rasg (_, instrs) ->
+                  List.fold_left
+                    (fun rasg instr ->
+                      let rasg, _, _ = aux rasg instr fvar in
+                      rasg)
+                    rasg
+                    instrs)
+                rasg
+                hl
+            in
+            let rasg'' = VSet.diff rasg rasg' in
+            ( rasg',
+              VSet.fold
+                (fun i spec ->
+                  add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec)
+                rasg''
+                instr.instr_spec,
+              fun v -> if VSet.mem v rasg'' then ghost_vd v else fvar v )
+          | _ ->
+            rasg, instr.instr_spec, fvar
+        in
+        let rasg, instr_spec, fvar = aux rasg instr fvar in
+        let instr_spec =
+          List.map (fun (t, b) -> instr_spec_replace fvar t, b) instr_spec
+        in
+        rasg, { instr with instr_spec } :: instrs, fvar)
+      (rasg, [], fun v -> v)
+      instrs
   in
   List.rev instrs
 
-module IntS = Set.Make(Int)
+module IntS = Set.Make (Int)
 
 let add_assigned k v =
   VMap.update v (function
-        | Some (n, ks) as b ->
-           if k > IntS.max_elt ks then Some (n + 1, IntS.add k ks) else b
-        | None -> Some (1, IntS.singleton k))
+      | Some (n, ks) as b ->
+        if k > IntS.max_elt ks then Some (n + 1, IntS.add k ks) else b
+      | None ->
+        Some (1, IntS.singleton k))
 
 let silly_asg i v =
   match v.value_desc with Var w -> w.var_id = i.var_id | _ -> false
@@ -1008,19 +1030,22 @@ let step_replace_var m reuse step =
       if silly_asg i v then asg else add_assigned k i asg
     | MStep (il, _, _) ->
       List.fold_right (add_assigned k) il asg
-    | MBranch (_, hl) ->
+    | MBranch (_, hl, _) ->
       List.fold_left
         (fun asg' (_, il) ->
-           let asg'' = List.fold_left (asg_instr k) asg il in
-           VMap.union (fun _ n1 n2 -> Some (max n1 n2)) asg' asg'')
+          let asg'' = List.fold_left (asg_instr k) asg il in
+          VMap.union (fun _ n1 n2 -> Some (max n1 n2)) asg' asg'')
         VMap.empty
         hl
-    | _ -> asg
+    | _ ->
+      asg
   in
   let assigned asg instrs =
-    let asg, _ = List.fold_left (fun (asg, k) instr ->
-        asg_instr k asg instr, k + 1)
-        (asg, 0) instrs
+    let asg, _ =
+      List.fold_left
+        (fun (asg, k) instr -> asg_instr k asg instr, k + 1)
+        (asg, 0)
+        instrs
     in
     asg
   in
@@ -1029,7 +1054,8 @@ let step_replace_var m reuse step =
   (* register the locations of assignments *)
   let asg = assigned VMap.empty step_instrs in
   (* let pp fmt (k, s) = *)
-  (*   Format.(fprintf fmt "%n{@[%a}@]" k (pp_comma_list pp_print_int) (IntS.elements s)) *)
+  (* Format.(fprintf fmt "%n{@[%a}@]" k (pp_comma_list pp_print_int)
+     (IntS.elements s)) *)
   (* in *)
   (* Format.printf "AVANT %a@." (VMap.pp pp) asg; *)
   (* SSA *)
@@ -1038,8 +1064,11 @@ let step_replace_var m reuse step =
      ones appearing *after* the original one *)
   let asg = assigned asg step_instrs in
   (* Format.printf "APRES %a@." (VMap.pp pp) asg; *)
-  let rasg = VMap.fold (fun v (n, _) rasg ->
-      if n > 1 then VSet.add v rasg else rasg) asg VSet.empty
+  let rasg =
+    VMap.fold
+      (fun v (n, _) rasg -> if n > 1 then VSet.add v rasg else rasg)
+      asg
+      VSet.empty
   in
   (* not SSA anymore *)
   let step_instrs = add_ghost_assigns_reassigned rasg step_instrs in
@@ -1052,8 +1081,12 @@ let machine_replace_variables reuse m =
 let pp_reuse fmt reuse =
   let l = Hashtbl.to_seq reuse |> List.of_seq in
   let pp_fun fmt (x, v) = Format.fprintf fmt "%s --> %s" x v.var_id in
-  Format.(fprintf fmt "{ @[<v 2>%a@] }"
-       (pp_print_list ~pp_sep:pp_print_comma pp_fun) l)
+  Format.(
+    fprintf
+      fmt
+      "{ @[<v 2>%a@] }"
+      (pp_print_list ~pp_sep:pp_print_comma pp_fun)
+      l)
 
 let machine_reuse_variables reuse m =
   (* Some outputs may have been replaced by locals. We reverse such bindings. *)
@@ -1106,7 +1139,7 @@ let rec instr_assign res instr =
     Disjunction.CISet.add i res
   | MStateAssign (i, _) ->
     Disjunction.CISet.add i res
-  | MBranch (_, hl) ->
+  | MBranch (_, hl, _) ->
     List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
   | MStep (il, _, _) ->
     List.fold_right Disjunction.CISet.add il res
@@ -1120,7 +1153,7 @@ let rec instr_constant_assign var instr =
   | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
   | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
     i = var
-  | MBranch (_, hl) ->
+  | MBranch (_, hl, _) ->
     List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
   | _ ->
     false
@@ -1136,17 +1169,16 @@ and instrs_constant_assign var instrs =
 
 let rec instr_reduce m v branches instr1 cont =
   match get_instr_desc instr1 with
-  | MLocalAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t) )
-  | MStateAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t) ) ->
+  | MLocalAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t))
+  | MStateAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t)) ->
     mkinstr ~instr_spec:(add_ghost_assign_spec v t []) (assign_comment m v t)
-    ::
-    instr1 :: (List.assoc c branches @ cont)
-  | MBranch (g, hl) ->
+    :: instr1
+    :: (List.assoc c branches @ cont)
+  | MBranch (g, hl, e) ->
     update_instr_desc
       instr1
-      (MBranch (g, List.map (fun (h, b) ->
-           h,
-           instrs_reduce m v branches b []) hl))
+      (MBranch
+         (g, List.map (fun (h, b) -> h, instrs_reduce m v branches b []) hl, e))
     :: cont
   | _ ->
     instr1 :: cont
@@ -1166,10 +1198,12 @@ let rec instrs_fusion m instrs =
     false, instrs
   | i1 :: i2 :: q -> (
     match i2.instr_desc with
-    | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
+    | MBranch ({ value_desc = Var v; _ }, hl, _) when instr_constant_assign v i1
+      ->
       ( true,
         instr_reduce
-          m v
+          m
+          v
           (List.map (fun (h, b) -> h, snd (instrs_fusion m b)) hl)
           { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
           (snd (instrs_fusion m q)) )
@@ -1205,15 +1239,25 @@ let machines_fusion prog =
 let machine_clean m =
   let unused = Machine_code_dep.compute_unused_variables m in
   let is_unused unused v = ISet.mem v.var_id unused in
-  (* unused that are written by a step call are not unused if they are not all unused *)
-  let unused = List.fold_left (fun unused instr ->
-      match get_instr_desc instr with
-      | MStep (xs, _, _) ->
-        begin match List.partition (is_unused unused) xs with
-          | _, [] -> unused
-          | xs, _ -> List.fold_left (fun unused v -> ISet.remove v.var_id unused) unused xs
-        end
-      | _ -> unused) unused m.mstep.step_instrs
+  (* unused that are written by a step call are not unused if they are not all
+     unused *)
+  let unused =
+    List.fold_left
+      (fun unused instr ->
+        match get_instr_desc instr with
+        | MStep (xs, _, _) -> (
+          match List.partition (is_unused unused) xs with
+          | _, [] ->
+            unused
+          | xs, _ ->
+            List.fold_left
+              (fun unused v -> ISet.remove v.var_id unused)
+              unused
+              xs)
+        | _ ->
+          unused)
+      unused
+      m.mstep.step_instrs
   in
   Log.report ~level:1 (fun fmt ->
       Format.fprintf
@@ -1231,14 +1275,12 @@ let machine_clean m =
         match get_instr_desc instr with
         | MLocalAssign (v, _) ->
           if is_used v then Some instr else None
-        | MStep (xs, _, _) when List.for_all is_unused xs -> None
-        | MBranch (e, hl) ->
+        | MStep (xs, _, _) when List.for_all is_unused xs ->
+          None
+        | MBranch (e, hl, ex) ->
           let hl = List.map (fun (h, l) -> h, filter_instrs l) hl in
-          if List.for_all (fun (_, l) -> l = []) hl then None else
-            Some
-              (update_instr_desc
-                 instr
-                 (MBranch (e, hl)))
+          if List.for_all (fun (_, l) -> l = []) hl then None
+          else Some (update_instr_desc instr (MBranch (e, hl, ex)))
         | _ ->
           Some instr)
       instrs