diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 8164c4e1ca08bbda6fe2f7600c50616b8d28bf76..731cc8be7a9e2e0dc4dcd582e7f6e939be7ec8fe 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -450,7 +450,7 @@ module PrintSpec = struct
     | GhostAssign (v1, v2) ->
       pp_ghost (pp_assign m mem_in (pp_c_var_read m)) fmt (v1, v2)
 
-  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
+  (* let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool *)
 
   let val_of_expr = function
     | Val v ->
@@ -1159,8 +1159,8 @@ module SrcMod = struct
   let pp_contract_arrow_step_name fmt =
     fprintf fmt "%s_step_ghost" Arrow.arrow_id
 
-  let pp_arrow_reset_ghost mem fmt inst =
-    fprintf fmt "%t(%a)" pp_contract_arrow_reset_name pp_indirect' (mem, inst)
+  (* let pp_arrow_reset_ghost mem fmt inst = *)
+  (*   fprintf fmt "%t(%a)" pp_contract_arrow_reset_name pp_indirect' (mem, inst) *)
 
   let pp_is_contract = pp_is_contract
 
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 5dbfcdf7f53f8f2198b00814cf38da41e374de87..5e0fad4cdc1e3f8ad0516061a09d118f812cbe07 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -59,7 +59,7 @@ module EmptyMod = struct
   module GhostProto = EmptyGhostProto
 
   let pp_import_spec_prototype _ _ = ()
-  let pp_set_reset_spec _ _ _ _ _ = ()
+  (* let pp_set_reset_spec _ _ _ _ _ = () *)
   let pp_clear_reset_spec _ _ _ _ = ()
   let pp_ghost_reset_spec _ _ _ _ = ()
   let pp_step_spec _ _ _ _ _ = ()
diff --git a/src/machine_code.ml b/src/machine_code.ml
index a4c4318f79c43fbfd6ae917b8577c9e241c0211b..5e5e956b67fa141131e1a35542b2b483c227f609 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -21,8 +21,6 @@ open Utils
 
 exception NormalizationError
 
-let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int
-
 (* Questions:
 
    - where are used the mconst. They contain initialization of constant in
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index ae6c48d6b03fc0ee1d88273116d4c89602accb9c..cb8833d20b0917989dc02a8683af1a382c2ba46d 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -165,48 +165,48 @@ let rec eliminate m elim instr =
          ( e_val g,
            List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
 
-let rec fv_value m s v =
-  match v.value_desc with
-  | Var v ->
-    if is_memory m v then s else VSet.add v s
-  | Fun (_, vl) | Array vl ->
-    List.fold_left (fv_value m) s vl
-  | Access (v1, v2) | Power (v1, v2) ->
-    fv_value m (fv_value m s v1) v2
-  | _ ->
-    s
-
-let fv_expr m s = function
-  | Val v ->
-    fv_value m s v
-  | Var v ->
-    if is_memory m v then s else VSet.add v s
-  | _ ->
-    s
-
-let fv_predicate m s = function
-  | Transition (_, _, _, _, vars, _, _, _) ->
-    List.fold_left (fv_expr m) s vars
-  | _ ->
-    s
-
-let rec fv_formula m s = function
-  | Equal (e1, e2) | GEqual (e1, e2) ->
-    fv_expr m (fv_expr m s e1) e2
-  | And f | Or f ->
-    List.fold_left (fv_formula m) s f
-  | Imply (a, b) | ExistsMem (_, a, b) ->
-    fv_formula m (fv_formula m s a) b
-  | Exists (xs, a) | Forall (xs, a) ->
-    VSet.filter (fun v -> not (List.mem v xs)) (fv_formula m s a)
-  | Ternary (e, a, b) ->
-    fv_expr m (fv_formula m (fv_formula m s a) b) e
-  | Predicate p ->
-    fv_predicate m s p
-  | Value v ->
-    fv_value m s v
-  | _ ->
-    s
+(* let rec fv_value m s v = *)
+(*   match v.value_desc with *)
+(*   | Var v -> *)
+(*     if is_memory m v then s else VSet.add v s *)
+(*   | Fun (_, vl) | Array vl -> *)
+(*     List.fold_left (fv_value m) s vl *)
+(*   | Access (v1, v2) | Power (v1, v2) -> *)
+(*     fv_value m (fv_value m s v1) v2 *)
+(*   | _ -> *)
+(*     s *)
+
+(* let fv_expr m s = function *)
+(*   | Val v -> *)
+(*     fv_value m s v *)
+(*   | Var v -> *)
+(*     if is_memory m v then s else VSet.add v s *)
+(*   | _ -> *)
+(*     s *)
+
+(* let fv_predicate m s = function *)
+(*   | Transition (_, _, _, _, vars, _, _, _) -> *)
+(*     List.fold_left (fv_expr m) s vars *)
+(*   | _ -> *)
+(*     s *)
+
+(* let rec fv_formula m s = function *)
+(*   | Equal (e1, e2) | GEqual (e1, e2) -> *)
+(*     fv_expr m (fv_expr m s e1) e2 *)
+(*   | And f | Or f -> *)
+(*     List.fold_left (fv_formula m) s f *)
+(*   | Imply (a, b) | ExistsMem (_, a, b) -> *)
+(*     fv_formula m (fv_formula m s a) b *)
+(*   | Exists (xs, a) | Forall (xs, a) -> *)
+(*     VSet.filter (fun v -> not (List.mem v xs)) (fv_formula m s a) *)
+(*   | Ternary (e, a, b) -> *)
+(*     fv_expr m (fv_formula m (fv_formula m s a) b) e *)
+(*   | Predicate p -> *)
+(*     fv_predicate m s p *)
+(*   | Value v -> *)
+(*     fv_value m s v *)
+(*   | _ -> *)
+(*     s *)
 
 let eliminate_transition m elim t =
   (* let tvars = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) t.tvars