diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 7e3267f4cd92aff576f623ed76b12ef726fd1704..b03c4c24a6562c1f7933aa9299c3a59ae2da1186 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -422,8 +422,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
                   e
                   (List.length hl)))
             hl
+      | MSpec "" ->
+        ()
       | MSpec s ->
         fprintf fmt "@[/*@@ %s */@]@ " s
+      | MComment "" ->
+        ()
       | MComment s ->
         fprintf fmt "/* %s */" s
     in
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index cde625bc4a469f8ce49cc05c30ff405353d58929..86445bdfca3e5994bc19962dfbbfbc57ebaa7b47 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -787,7 +787,8 @@ and instrs_are_skip instrs = List.for_all instr_is_skip instrs
 let instr_cons instr cont =
   match instr_is_skip instr, cont with
   | true, [] ->
-    [ { instr with instr_desc = MComment "" } ]
+    if instr.instr_spec = [] then []
+    else [ { instr with instr_desc = MComment "" } ]
   | true, i :: cont ->
     { i with instr_spec = i.instr_spec @ instr.instr_spec } :: cont
   | false, _ ->
@@ -927,36 +928,6 @@ let rec add_ghost_assign fvar instr =
     instr
 
 and add_ghost_assigns fvar = List.map (add_ghost_assign fvar)
-(* let is_reused_def v = Hashtbl.find_opt reuse v.var_id in *)
-(* let add_reused vars i = *)
-(*   let v = fvar i in *)
-(*   if v.var_id = i.var_id then vars else VMap.add i v vars *)
-(* in *)
-(* let rec is_defining_reused vars instr = *)
-(*   match instr.instr_desc with *)
-(*   | 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 *)
-(* in *)
-(* 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 *)
-(*     in *)
-(*     { instr with instr_spec }) *)
-(*   instrs *)
 
 let ghost_vd v = { v with var_id = "__" ^ v.var_id }
 
@@ -968,47 +939,50 @@ let add_ghost_assigns_reassigned rasg instrs =
           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,
+              {
+                instr with
+                instr_spec =
+                  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' =
+            let rasg, instr_spec, fvar =
+              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
+            in
+            rasg, { instr with instr_spec }, fvar
+          | MBranch (e, hl, b) ->
+            let rasg, fvar, hl =
               List.fold_left
-                (fun rasg (_, instrs) ->
-                  List.fold_left
-                    (fun rasg instr ->
-                      let rasg, _, _ = aux rasg instr fvar in
-                      rasg)
-                    rasg
-                    instrs)
-                rasg
+                (fun (rasg, fvar, hl) (h, l) ->
+                  let rasg, fvar, l =
+                    List.fold_left
+                      (fun (rasg, fvar, l) i ->
+                        let rasg, i, fvar = aux rasg i fvar in
+                        rasg, fvar, i :: l)
+                      (rasg, fvar, [])
+                      l
+                  in
+                  rasg, fvar, (h, List.rev l) :: hl)
+                (rasg, fvar, [])
                 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 with instr_desc = MBranch (e, List.rev hl, b) }, fvar
           | _ ->
-            rasg, instr.instr_spec, fvar
+            rasg, instr, fvar
         in
-        let rasg, instr_spec, fvar = aux rasg instr fvar in
+        let rasg, instr, fvar = aux rasg instr fvar in
         let instr_spec =
-          List.map (fun (t, b) -> instr_spec_replace fvar t, b) instr_spec
+          List.map (fun (t, b) -> instr_spec_replace fvar t, b) instr.instr_spec
         in
         rasg, { instr with instr_spec } :: instrs, fvar)
       (rasg, [], fun v -> v)