diff --git a/src/lib/structures/profiling.ml b/src/lib/structures/profiling.ml
index c346688ffd..fb4e8a28fc 100644
--- a/src/lib/structures/profiling.ml
+++ b/src/lib/structures/profiling.ml
@@ -45,56 +45,67 @@ type inst_info = {
 }
 
 type t = {
-  decisions : int ref;
-  assumes : int ref;
-  assumes_current_lvl : int ref;
-  queries : int ref;
-  instantiation_rounds : int ref;
-  instances : int ref;
-  decision_lvl : int ref;
-  instantiation_lvl : int ref;
-
+  mutable decisions : int;
+  mutable assumes : int;
+  mutable assumes_current_lvl : int;
+  mutable queries : int;
+  mutable instantiation_rounds : int;
+  mutable instances : int;
+  mutable decision_lvl : int;
+  mutable instantiation_lvl : int;
   (* 4 kinds of conflicts *)
-  th_conflicts : int ref;
-  b_conflicts : int ref;
-  bcp_th_conflicts : int ref;
-  bcp_b_conflicts : int ref;
-  bcp_mix_conflicts : int ref;
-
+  mutable th_conflicts : int;
+  mutable b_conflicts : int;
+  mutable bcp_th_conflicts : int;
+  mutable bcp_b_conflicts : int;
+  mutable bcp_mix_conflicts : int;
   (* 4 kinds of red/elim *)
-  t_red : int ref;
-  b_red : int ref;
-  t_elim : int ref;
-  b_elim : int ref;
-  (* first int: counter ok kept instances,
-     second int: counter of removed instances*)
-  instances_map : inst_info MS.t ref;
-  instances_map_printed : bool ref
+  mutable t_red : int;
+  mutable b_red : int;
+  mutable t_elim : int;
+  mutable b_elim : int;
+  mutable instances_map : inst_info MS.t;
+  mutable instances_map_printed : bool;
 }
 
+type mode =
+  | Stats
+  | Timers
+  | CallTree
+  | FunctionsTimers
+  | Instances
+
+let mode = ref Stats
+
+let max_nb_prints = 30
+
+let nb_prints = ref max_nb_prints
+
+let initial_info = ref true
+
 let state = {
-  decisions = ref 0;
-  assumes = ref 0;
-  assumes_current_lvl = ref 0;
-  queries = ref 0;
-  instantiation_rounds = ref 0;
-  instances = ref 0;
-  decision_lvl = ref 0;
-  instantiation_lvl = ref 0;
-
-  th_conflicts = ref 0;
-  b_conflicts = ref 0;
-  bcp_th_conflicts = ref 0;
-  bcp_b_conflicts = ref 0;
-  bcp_mix_conflicts = ref 0;
-
-  t_red  = ref 0;
-  b_red  = ref 0;
-  t_elim = ref 0;
-  b_elim = ref 0;
-
-  instances_map = ref MS.empty;
-  instances_map_printed = ref false
+  decisions = 0;
+  assumes = 0;
+  assumes_current_lvl = 0;
+  queries = 0;
+  instantiation_rounds = 0;
+  instances = 0;
+  decision_lvl = 0;
+  instantiation_lvl = 0;
+
+  th_conflicts = 0;
+  b_conflicts = 0;
+  bcp_th_conflicts = 0;
+  bcp_b_conflicts = 0;
+  bcp_mix_conflicts = 0;
+
+  t_red = 0;
+  b_red = 0;
+  t_elim = 0;
+  b_elim = 0;
+
+  instances_map = MS.empty;
+  instances_map_printed = false
 }
 
 let set_sigprof () =
@@ -107,67 +118,74 @@ let set_sigprof () =
        { Unix.it_value = tm; Unix.it_interval = 0. })
 
 let init () =
-  state.decisions := 0;
-  state.assumes := 0;
-  state.queries := 0;
-  state.instantiation_rounds := 0;
-  state.instances := 0;
-  state.decision_lvl := 0;
-  state.instantiation_lvl := 0;
-  state.assumes_current_lvl := 0;
-  state.th_conflicts := 0;
-  state.b_conflicts := 0;
-  state.bcp_th_conflicts := 0;
-  state.bcp_b_conflicts := 0;
-  state.bcp_mix_conflicts := 0;
-  state.t_red  := 0;
-  state.b_red  := 0;
-  state.t_elim := 0;
-  state.b_elim := 0;
-  state.instances_map := MS.empty;
-  state.instances_map_printed := false;
+  state.decisions <- 0;
+  state.assumes <- 0;
+  state.queries <- 0;
+  state.instantiation_rounds <- 0;
+  state.instances <- 0;
+  state.decision_lvl <- 0;
+  state.instantiation_lvl <- 0;
+  state.assumes_current_lvl <- 0;
+  state.th_conflicts <- 0;
+  state.b_conflicts <- 0;
+  state.bcp_th_conflicts <- 0;
+  state.bcp_b_conflicts <- 0;
+  state.bcp_mix_conflicts <- 0;
+  state.t_red <- 0;
+  state.b_red <- 0;
+  state.t_elim <- 0;
+  state.b_elim <- 0;
+  state.instances_map <- MS.empty;
+  state.instances_map_printed <- false;
   set_sigprof ()
 
 (* update functions of the internal state *)
 
 let assume nb =
-  state.assumes := nb + !(state.assumes);
-  state.assumes_current_lvl := nb + !(state.assumes_current_lvl)
+  state.assumes <- nb + state.assumes;
+  state.assumes_current_lvl <- nb + state.assumes_current_lvl
 
-let query () =
-  incr state.queries
+let query () = state.queries <- state.queries + 1
 
 let instances l =
-  state.instances := !(state.instances) + List.length l
+  state.instances <- state.instances + List.length l
 
 let instantiation ilvl =
-  incr state.instantiation_rounds;
-  incr state.instantiation_lvl;
-  if not (!(state.instantiation_lvl) = ilvl) then begin
+  state.instantiation_rounds <- state.instantiation_rounds + 1;
+  state.instantiation_lvl <- state.instantiation_lvl + 1;
+  if not (state.instantiation_lvl = ilvl) then begin
     Printer.print_err
       "state.instantiation_lvl = %d et ilvl = %d"
-      !(state.instantiation_lvl) ilvl;
+      state.instantiation_lvl ilvl;
     assert false
   end
 
 let bool_conflict () =
-  incr state.b_conflicts
+  state.b_conflicts <- state.b_conflicts + 1
 
 let theory_conflict () =
-  incr state.th_conflicts
+  state.th_conflicts <- state.th_conflicts + 1
 
 let bcp_conflict b1 b2 =
-  if b1 && b2 then incr state.bcp_b_conflicts
-  else if (not b1) && (not b2) then incr state.bcp_th_conflicts
-  else incr state.bcp_mix_conflicts
+  if b1 && b2 then state.bcp_b_conflicts <- state.bcp_b_conflicts + 1
+  else if (not b1) && (not b2) then state.bcp_th_conflicts <- state.bcp_th_conflicts + 1
+  else state.bcp_mix_conflicts <- state.bcp_mix_conflicts + 1
 
-let red b = if b then incr state.b_red else incr state.t_red
+let red b =
+  if b then
+    state.b_red <- state.b_red + 1
+  else
+    state.t_red <- state.t_red + 1
 
-let elim b = if b then incr state.b_elim else incr state.t_elim
+let elim b =
+  if b then
+    state.b_elim <- state.b_elim + 1
+  else
+    state.t_elim <- state.t_elim + 1
 
-let reset_ilevel n = state.instantiation_lvl := n
+let reset_ilevel n = state.instantiation_lvl <- n
 
-let reset_dlevel n = state.decision_lvl := n
+let reset_dlevel n = state.decision_lvl <- n
 
 let empty_inst_info loc =
   {
@@ -184,9 +202,9 @@ let empty_inst_info loc =
   }
 
 let new_instance_of axiom inst loc kept =
-  let () = state.instances_map_printed := false in
+  let () = state.instances_map_printed <- false in
   let ii =
-    try MS.find axiom !(state.instances_map)
+    try MS.find axiom state.instances_map
     with Not_found -> empty_inst_info loc
   in
   assert (ii.loc == loc);
@@ -196,44 +214,47 @@ let new_instance_of axiom inst loc kept =
     else
       {ii with ignored = ii.ignored + 1}
   in
-  state.instances_map := MS.add axiom ii !(state.instances_map)
+  state.instances_map <- MS.add axiom ii state.instances_map
 
 let conflicting_instance axiom loc =
   let ii =
-    try MS.find axiom !(state.instances_map)
+    try MS.find axiom state.instances_map
     with Not_found -> empty_inst_info loc
   in
   let ii = {ii with confl = ii.confl + 1} in
   assert (ii.loc == loc);
-  state.instances_map := MS.add axiom ii !(state.instances_map)
+  state.instances_map <- MS.add axiom ii state.instances_map
 
 let decision_on_instance axiom_name =
   try
     let ii =
-      MS.find axiom_name !(state.instances_map)
+      MS.find axiom_name state.instances_map
     in
     let ii = {ii with decided = ii.decided + 1} in
     (*assert (ii.loc == loc);*)
-    state.instances_map := MS.add axiom_name ii !(state.instances_map)
+    state.instances_map <- MS.add axiom_name ii state.instances_map
   with Not_found -> ()
 
 
 let decision d origin =
-  incr state.decisions;
-  incr state.decision_lvl;
-  if not (!(state.decision_lvl) = d) then begin
+  state.decisions <- state.decisions + 1;
+  state.decision_lvl <- state.decision_lvl + 1;
+  if state.decision_lvl <> d then begin
     Printer.print_err
       "state.decision_lvl = %d et d = %d"
-      !(state.decision_lvl) d;
+      state.decision_lvl d;
+    (* TODO(Steven): if nobody knows how to use the previous print to debug
+       anything, I suggest we either remove `d` or get rid the invariant:
+       #(calls to Profiling.decision) = d. *)
     assert false
   end;
-  state.assumes_current_lvl := 0;
+  state.assumes_current_lvl <- 0;
   decision_on_instance origin
 
 
 let register_produced_terms axiom loc consumed all produced _new =
   let ii =
-    try MS.find axiom !(state.instances_map)
+    try MS.find axiom state.instances_map
     with Not_found -> empty_inst_info loc
   in
   assert (ii.loc == loc);
@@ -244,27 +265,12 @@ let register_produced_terms axiom loc consumed all produced _new =
      produced = SE.union ii.produced produced;
      _new     = SE.union ii._new _new }
   in
-  state.instances_map := MS.add axiom ii !(state.instances_map)
+  state.instances_map <- MS.add axiom ii state.instances_map
 
 (******************************************************************************
    printing the internal state
  ******************************************************************************)
 
-type mode =
-  | Stats
-  | Timers
-  | CallTree
-  | FunctionsTimers
-  | Instances
-
-let mode = ref Stats
-
-let max_nb_prints = 30
-
-let nb_prints = ref max_nb_prints
-
-let initial_info = ref true
-
 let string_resize s i =
   let sz = max 0 (i - (String.length s)) in
   let tmp = String.make sz ' ' in
@@ -277,7 +283,15 @@ let float_resize f i = string_resize (Format.sprintf "%f" f) i
 let percent total a =
   (string_of_int (int_of_float (a *. 100. /. total))) ^ "%"
 
-let columns =
+(* Profiling columns:
+   - Name
+   - Description
+   - Length of the cell
+   - Is the column linked to a statistic (Some true), a timer (Some false) or
+     not (None)?
+   - To be discovered
+*)
+let columns : (string * string * int * bool option * 'a) list =
   [
     "GTimer", "Global timer", 11, None,
     (fun _ gtime _ sz -> float_resize gtime sz);
@@ -311,63 +325,63 @@ let columns =
     (*-----------------------------------------------------------------*)
 
     "ilvl", "Current Instantiaton level", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.instantiation_lvl) sz);
+    (fun _ _ _ sz -> int_resize state.instantiation_lvl sz);
 
     "#i rnds", "Number of intantiation rounds", 8, Some true,
     (fun _ _ _ sz ->
-       int_resize !(state.instantiation_rounds) sz);
+       int_resize state.instantiation_rounds sz);
 
 
     "#insts", "Number of generated instances", 8, Some true,
-    (fun _ _ _ sz -> int_resize !(state.instances) sz);
+    (fun _ _ _ sz -> int_resize state.instances sz);
 
     "i/r", "AVG number of generated instances per instantiation rounds",
     8, Some true,
     (fun _ _ _ sz ->
        int_resize
-         (!(state.instances) / (max 1 !(state.instantiation_rounds))) sz);
+         (state.instances / (max 1 state.instantiation_rounds)) sz);
 
     "dlvl", "Current Decision level", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.decision_lvl) sz);
+    (fun _ _ _ sz -> int_resize state.decision_lvl sz);
 
     "#decs", "Number of decisions", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.decisions) sz);
+    (fun _ _ _ sz -> int_resize state.decisions sz);
 
     "T-asm", "Number of calls to Theory.assume", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.assumes) sz);
+    (fun _ _ _ sz -> int_resize state.assumes sz);
 
     "T/d", "Number of Theory.assume after last decision", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.assumes_current_lvl) sz);
+    (fun _ _ _ sz -> int_resize state.assumes_current_lvl sz);
 
     "T-qr", "Number of calls to Theory.query", 15, Some true,
-    (fun _ _ _ sz -> int_resize !(state.queries) sz);
+    (fun _ _ _ sz -> int_resize state.queries sz);
 
     "B-R", "Number of reduced clauses by Boolean propagation", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.b_red) sz);
+    (fun _ _ _ sz -> int_resize state.b_red sz);
 
     "B-E", "Number of eliminated clauses by Boolean propagation", 6,
-    Some true, (fun _ _ _ sz -> int_resize !(state.b_elim) sz);
+    Some true, (fun _ _ _ sz -> int_resize state.b_elim sz);
 
     "T-R", "Number of reduced clauses by Theory propagation", 6, Some true,
-    (fun _ _ _ sz -> int_resize !(state.t_red) sz);
+    (fun _ _ _ sz -> int_resize state.t_red sz);
 
     "T-E", "Number of eliminated clauses by Theory propagation", 6,
-    Some true, (fun _ _ _ sz -> int_resize !(state.t_elim) sz);
+    Some true, (fun _ _ _ sz -> int_resize state.t_elim sz);
 
     "B-!",  "Number of direct Boolean conflicts", 5, Some true,
-    (fun _ _ _ sz -> int_resize !(state.b_conflicts) sz);
+    (fun _ _ _ sz -> int_resize state.b_conflicts sz);
 
     "T-!", "Number of direct Theory conflicts" , 5, Some true,
-    (fun _ _ _ sz -> int_resize !(state.th_conflicts) sz);
+    (fun _ _ _ sz -> int_resize state.th_conflicts sz);
 
     "B>!", "Number of Boolean conflicts deduced by BCP", 5, Some true,
-    (fun _ _ _ sz -> int_resize !(state.bcp_b_conflicts) sz);
+    (fun _ _ _ sz -> int_resize state.bcp_b_conflicts sz);
 
     "T>!", "Number of Theory conflicts deduced by BCP", 5, Some true,
-    (fun _ _ _ sz -> int_resize !(state.bcp_th_conflicts) sz);
+    (fun _ _ _ sz -> int_resize state.bcp_th_conflicts sz);
 
     "M>!", "Number of Mix conflicts deduced by BCP", 5, Some true,
-    (fun _ _ _ sz -> int_resize !(state.bcp_mix_conflicts) sz);
+    (fun _ _ _ sz -> int_resize state.bcp_mix_conflicts sz);
 
     (*-----------------------------------------------------------------*)
     "SAT", "Time spent in SAT module(s)", 16, Some false,
@@ -448,23 +462,24 @@ let print_initial_info fmt =
 
 let stats_limit, timers_limit =
   let aux tmp sz =
-    tmp := Format.sprintf "%s|" !tmp;
-    for _ = 1 to sz do tmp := Format.sprintf "%s-" !tmp done
+    tmp := Format.sprintf "%s%s|" !tmp (String.make (max 0 sz) '-');
   in
-  let tmp_s = ref "" in
-  let tmp_t = ref "" in
+  let tmp_s = ref "|" in
+  let tmp_t = ref "|" in
   List.iter
     (fun (_, _, sz, opt, _) ->
        match opt with
        | Some true  -> aux tmp_s sz
        | Some false -> aux tmp_t sz
        | _          -> aux tmp_s sz; aux tmp_t sz
-    )columns;
-  !tmp_s ^ "|", !tmp_t ^ "|"
+    )
+    columns;
+  !tmp_s, !tmp_t
 
 let print_header header fmt =
   let pp_stats =
-    match !mode with Stats -> true | Timers -> false | _ -> assert false in
+    match !mode with Stats -> true | Timers -> false | _ -> assert false
+  in
   if header || !nb_prints >= max_nb_prints then begin
     nb_prints := 0;
     Format.fprintf fmt "%s@." (if pp_stats then stats_limit else timers_limit);
@@ -502,32 +517,13 @@ let print_timers header steps fmt timers =
     )columns;
   Format.fprintf fmt "|@."
 
-(* unused
-   let report2 axiom fmt (b,e) =
-   let open Lexing in
-   let l = b.pos_lnum in
-   let fc = b.pos_cnum - b.pos_bol + 1 in
-   let lc = e.pos_cnum - b.pos_bol + 1 in
-   fprintf fmt "(Sub) Axiom \"%s\", line %d, characters %d-%d:"
-    axiom l fc lc
-*)
-
-(* unused
-   let report3 fmt (b,e) =
-   let open Lexing in
-   let l = b.pos_lnum in
-   let fc = b.pos_cnum - b.pos_bol + 1 in
-   let lc = e.pos_cnum - b.pos_bol + 1 in
-   fprintf fmt "line %d, chars %d-%d." l fc lc
-*)
-
-let (@@) a b = if a <> 0 then a else b
 
 let print_instances_generation forced _steps fmt _timers =
-  if not forced && !(state.instances_map_printed) then
+  let (@@) a b = if a <> 0 then a else b in
+  if not forced && state.instances_map_printed then
     Format.fprintf fmt "[Instances profiling] No change since last print@."
   else
-    let () = state.instances_map_printed := true in
+    let () = state.instances_map_printed <- true in
     if not forced then ignore(Sys.command("clear"));
     Format.fprintf fmt "[Instances profiling] ...@.";
     let insts =
@@ -538,7 +534,7 @@ let print_instances_generation forced _steps fmt _timers =
            let ratio = f1 /. (f1 +. f2) in
            let all_card = SE.cardinal ii.all_insts in
            (name, ii, all_card, ratio) :: acc)
-        !(state.instances_map) []
+        state.instances_map []
     in
     let insts =
       List.fast_sort (fun (_, i1, c1, _) (_, i2, c2, _) ->
@@ -566,54 +562,8 @@ let print_instances_generation forced _steps fmt _timers =
          fprintf fmt "new: %s|| "
            (int_resize (SE.cardinal i._new) 5);
          fprintf fmt "%s" (string_resize name 30);
-         (*fprintf fmt "%s | " (string_resize name 30);
-           fprintf fmt "%a@." report3 i.loc (* too long *) *)
          fprintf fmt "@."
       )insts;
-    (*if forced then
-      let () = fprintf fmt "digraph v{@." in
-      fprintf fmt "size=\"10,7.5\"@.";
-      fprintf fmt "ratio=\"fill\"@.";
-      fprintf fmt "rotate=90@.";
-      fprintf fmt "fontsize=\"12pt\"@.";
-      fprintf fmt "rankdir = TB@." ;
-      let terms = ref SE.empty in
-      List.iter
-      (fun (name, i, _) ->
-      SE.iter
-      (fun t ->
-      fprintf fmt "\"%d\" -> \"%s\";@." (T.hash t) name
-      )i.consumed;
-      terms := SE.union !terms i.consumed;
-      SE.iter
-      (fun t ->
-      fprintf fmt "\"%s\" -> \"%d\";@." name (T.hash t)
-      )i._new;
-      terms := SE.union !terms i._new;
-      fprintf fmt "\"%s\" [fillcolor=yellow];@." name;
-      )insts;
-      SE.iter
-      (fun t ->
-      fprintf fmt "\"%d\" [fillcolor=green];@." (T.hash t);
-      )!terms;
-      fprintf fmt "}@."*)
-    (*
-      if forced then
-      let () = fprintf fmt "digraph v{@." in
-      fprintf fmt "size=\"10,7.5\"@.";
-      fprintf fmt "ratio=\"fill\"@.";
-      fprintf fmt "rotate=90@.";
-      fprintf fmt "fontsize=\"12pt\"@.";
-      fprintf fmt "rankdir = TB@." ;
-      List.iter
-      (fun (s1, i1, _) ->
-      List.iter
-      (fun (s2, i2, _) ->
-      if SE.is_empty (SE.inter i1.produced i2.consumed) then ()
-      else fprintf fmt "\"%s\" -> \"%s\";@." s1 s2
-      )insts
-      )insts;
-      fprintf fmt "}@."*)
     ()
 
 let print_call_tree _forced _steps fmt timers =
@@ -656,12 +606,12 @@ let float_print =
 
 let line_of_module =
   let open Format in
-  fun arr fmt f ->
+  fun timers fmt f ->
     fprintf fmt "%s " (string_resize (Timers.string_of_ty_function f) 13);
     let cpt = ref 0. in
     List.iter
       (fun m ->
-         let v = arr.(Timers.mtag m).(Timers.ftag f) in
+         let v = Timers.get_value timers m f in
          cpt := !cpt +. v;
          fprintf fmt "| %a  " float_print v
       ) Timers.all_modules;
@@ -694,10 +644,7 @@ let timers_table =
     fprintf fmt "|@.";
     for _ = 0 to 206 do fprintf fmt "-" done;
     fprintf fmt "|@.";
-    let arr_timers = Timers.get_timers_array timers in
-    List.iter
-      (line_of_module arr_timers fmt)
-      Timers.all_functions;
+    List.iter (line_of_module timers fmt) Timers.all_functions;
     line_of_sum_module fmt timers
 
 let print =
@@ -706,6 +653,7 @@ let print =
     print_initial_info fmt;
     set_sigprof();
     if all then begin
+      let old_mode = !mode in
       mode := Stats;
       fprintf fmt "@.";
       print_stats true steps fmt timers;
@@ -717,6 +665,7 @@ let print =
       fprintf fmt "@.";
       print_instances_generation true steps fmt timers;
       fprintf fmt "@.";
+      mode := old_mode
     end
     else match !mode with
       | Stats           -> print_stats false steps fmt timers
diff --git a/src/lib/structures/profiling.mli b/src/lib/structures/profiling.mli
index 9f4aa4d27e..b57d9dbd79 100644
--- a/src/lib/structures/profiling.mli
+++ b/src/lib/structures/profiling.mli
@@ -28,8 +28,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t
-
 val init : unit -> unit
 val decision : int -> string -> unit
 val assume : int -> unit
diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml
index 1ddbc40896..5a0b223004 100644
--- a/src/lib/util/timers.ml
+++ b/src/lib/util/timers.ml
@@ -45,24 +45,24 @@ type ty_module =
   | M_Simplex
   | M_Ite
 
-let mtag k = match k with
-  | M_None     -> 0
-  | M_Typing   -> 1
-  | M_Sat      -> 2
-  | M_Match    -> 3
-  | M_CC       -> 4
-  | M_UF       -> 5
-  | M_Arith    -> 6
-  | M_Arrays   -> 7
-  | M_Sum      -> 8
-  | M_Records  -> 9
-  | M_AC       -> 10
-  | M_Expr     -> 11
-  | M_Triggers -> 12
-  | M_Simplex  -> 13
-  | M_Ite      -> 14
-
-let nb_mtag = 14
+let all_modules = [
+  M_None;
+  M_Typing;
+  M_Sat;
+  M_Match;
+  M_CC;
+  M_UF;
+  M_Arith;
+  M_Arrays;
+  M_Sum;
+  M_Records;
+  M_AC;
+  M_Expr;
+  M_Triggers;
+  M_Simplex;
+  M_Ite
+]
+
 
 type ty_function =
   | F_add
@@ -86,29 +86,29 @@ type ty_function =
   | F_apply_subst
   | F_instantiate
 
-let ftag f = match f with
-  | F_add           -> 0
-  | F_add_lemma     -> 1
-  | F_assume        -> 2
-  | F_class_of      -> 3
-  | F_leaves        -> 4
-  | F_make          -> 5
-  | F_m_lemmas      -> 6
-  | F_m_predicates  -> 7
-  | F_query         -> 8
-  | F_solve         -> 9
-  | F_subst         -> 10
-  | F_union         -> 11
-  | F_unsat         -> 12
-  | F_add_predicate -> 13
-  | F_add_terms     -> 14
-  | F_are_equal     -> 15
-  | F_none          -> 16
-  | F_new_facts     -> 17
-  | F_apply_subst   -> 18
-  | F_instantiate   -> 19
-
-let nb_ftag = 20
+let all_functions = [
+  F_add;
+  F_add_lemma;
+  F_add_predicate;
+  F_add_terms;
+  F_are_equal;
+  F_assume;
+  F_class_of;
+  F_leaves;
+  F_make;
+  F_m_lemmas;
+  F_m_predicates;
+  F_query;
+  F_solve;
+  F_subst;
+  F_union;
+  F_unsat;
+  F_none;
+  F_new_facts;
+  F_apply_subst;
+  F_instantiate;
+]
+
 
 let string_of_ty_module k = match k with
   | M_None     -> "None"
@@ -149,6 +149,96 @@ let string_of_ty_function f = match f with
   | F_apply_subst   -> "apply_subst"
   | F_instantiate   -> "instantiate"
 
+module TimerTable = struct
+  module FTbl = Hashtbl.Make(
+    struct
+      type t = ty_function
+
+      let hash = function
+        | F_add           -> 0
+        | F_add_lemma     -> 1
+        | F_assume        -> 2
+        | F_class_of      -> 3
+        | F_leaves        -> 4
+        | F_make          -> 5
+        | F_m_lemmas      -> 6
+        | F_m_predicates  -> 7
+        | F_query         -> 8
+        | F_solve         -> 9
+        | F_subst         -> 10
+        | F_union         -> 11
+        | F_unsat         -> 12
+        | F_add_predicate -> 13
+        | F_add_terms     -> 14
+        | F_are_equal     -> 15
+        | F_none          -> 16
+        | F_new_facts     -> 17
+        | F_apply_subst   -> 18
+        | F_instantiate   -> 19
+
+      let equal t t' = hash t = hash t'
+    end)
+
+  module MTbl = Hashtbl.Make(
+    struct
+      type t = ty_module
+
+      let hash =
+        function
+        | M_None     -> 0
+        | M_Typing   -> 1
+        | M_Sat      -> 2
+        | M_Match    -> 3
+        | M_CC       -> 4
+        | M_UF       -> 5
+        | M_Arith    -> 6
+        | M_Arrays   -> 7
+        | M_Sum      -> 8
+        | M_Records  -> 9
+        | M_AC       -> 10
+        | M_Expr     -> 11
+        | M_Triggers -> 12
+        | M_Simplex  -> 13
+        | M_Ite      -> 14
+
+      let equal t t' = hash t = hash t'
+    end)
+
+  type t = float FTbl.t MTbl.t
+
+  let create = MTbl.create
+
+  let clear = MTbl.clear
+
+  (** Returns the timer value associated to the module [m]
+      and the function [f]. *)
+  let get t m f =
+    match MTbl.find_opt t m with
+    | None -> 0.
+    | Some t ->
+      match FTbl.find_opt t f with
+      | None -> 0.
+      | Some f -> f
+
+  (** Sets the timer value associated to the module [m]
+      and the function [f]. *)
+  let set t m f v =
+    let ftbl =
+      match MTbl.find_opt t m with
+      | None ->
+        let new_tbl = FTbl.create 1 in
+        MTbl.add t m new_tbl;
+        new_tbl
+      | Some tbl -> tbl
+    in
+    FTbl.add ftbl f v
+
+  let get_sum t m =
+    match MTbl.find_opt t m with
+    | None -> 0.
+    | Some ft -> FTbl.fold (fun _ -> (+.)) ft 0.
+end
+
 type t = {
   (* current time *)
   mutable cur_u : float;
@@ -160,7 +250,7 @@ type t = {
   mutable stack : (ty_module * ty_function * int) list;
 
   (* table of timers for each combination "" *)
-  z : (float array) array;
+  z : TimerTable.t ;
   (*h:(ty_module, float ref) Hashtbl.t;*)
 }
 
@@ -172,24 +262,19 @@ let empty () =
   { cur_t = (M_None, F_none, 0);
     cur_u = 0.0;
     stack = [];
-    z = Array.init nb_mtag (fun _ -> Array.make nb_ftag 0.);
+    z = TimerTable.create 5
   }
-
-
+  
 (** reset the references of the given env to empty **)
 let reset env =
-  for i = 0 to nb_mtag - 1 do
-    let a = env.z.(i) in for j = 0 to nb_ftag - 1 do a.(j) <- 0. done
-  done;
+  TimerTable.clear env.z;
   env.cur_t <- (M_None, F_none, 0);
   env.cur_u <- 0.0;
   env.stack <- [];
   cpt_id := 0
 
 let accumulate env cur m f =
-  let mt = mtag m in
-  let ft = ftag f in
-  env.z.(mt).(ft) <- env.z.(mt).(ft) +. (cur -. env.cur_u)
+  TimerTable.set env.z m f (cur -. env.cur_u)
 
 let accumulate_cumulative_mode name env m f cur =
   if Options.get_cumulative_time_profiling() then
@@ -245,70 +330,16 @@ let update env =
   accumulate env cur m f;
   env.cur_u <- cur
 
-(** get the value of the timer "m x f" **)
-let get_value env m f = env.z.(mtag m).(ftag f)
+(** Returns the value of the timer associated to the module and function. *)
+let get_value env m f = TimerTable.get env.z m f
 
 (** get the sum of the "ty_function" timers for the given "ty_module" **)
-let get_sum env m =
-  let cpt = ref 0. in
-  Array.iter (fun v -> cpt := !cpt +. v) env.z.(mtag m);
-  !cpt
+let get_sum env m = TimerTable.get_sum env.z m
 
 let current_timer env = env.cur_t
 
 let get_stack env = env.stack
 
-let get_timers_array env = env.z
-
-let all_functions =
-  let l =
-    [ F_add;
-      F_add_lemma;
-      F_add_predicate;
-      F_add_terms;
-      F_are_equal;
-      F_assume;
-      F_class_of;
-      F_leaves;
-      F_make;
-      F_m_lemmas;
-      F_m_predicates;
-      F_query;
-      F_solve;
-      F_subst;
-      F_union;
-      F_unsat;
-      F_none;
-      F_new_facts;
-      F_apply_subst;
-      F_instantiate;
-    ]
-  in
-  assert (List.length l = nb_ftag);
-  l
-
-let all_modules =
-  let l =
-    [ M_None;
-      M_Typing;
-      M_Sat;
-      M_Match;
-      M_CC;
-      M_UF;
-      M_Arith;
-      M_Arrays;
-      M_Sum;
-      M_Records;
-      M_AC;
-      M_Expr;
-      M_Triggers;
-      M_Simplex;
-    ]
-  in
-  assert (List.length l = nb_mtag);
-  l
-
-
 let (timer_start : (ty_module -> ty_function -> unit) ref) =
   ref (fun _ _ -> ())
 
diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli
index 1016d281ba..3f0cc5e8d5 100644
--- a/src/lib/util/timers.mli
+++ b/src/lib/util/timers.mli
@@ -99,12 +99,6 @@ val string_of_ty_function : ty_function -> string
 
 val get_stack : t -> (ty_module * ty_function * int) list
 
-val get_timers_array : t -> (float array) array
-
-val mtag : ty_module -> int
-
-val ftag : ty_function -> int
-
 val all_modules : ty_module list
 
 val all_functions : ty_function list