diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml index ad8f7e7c5..8e3036bb7 100644 --- a/src/lib/reasoners/ite_rel.ml +++ b/src/lib/reasoners/ite_rel.ml @@ -212,12 +212,12 @@ let assume env _ la = let assume env uf la = if Options.get_timers() then try - Timers.exec_timer_start Timers.M_Arrays Timers.F_assume; + Timers.exec_timer_start Timers.M_Ite Timers.F_assume; let res =assume env uf la in - Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume; + Timers.exec_timer_pause Timers.M_Ite Timers.F_assume; res with e -> - Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume; + Timers.exec_timer_pause Timers.M_Ite Timers.F_assume; raise e else assume env uf la diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index 648a53e61..1ddbc4089 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -43,22 +43,24 @@ type ty_module = | M_Expr | M_Triggers | 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_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 @@ -109,20 +111,21 @@ let ftag f = match f with let nb_ftag = 20 let string_of_ty_module k = match k with - | M_None -> "None" - | M_Typing -> "Typing" - | M_Sat -> "Sat" - | M_Match -> "Match" - | M_CC -> "CC" - | M_UF -> "UF" - | M_Arith -> "Arith" - | M_Arrays -> "Arrays" - | M_Sum -> "Sum" - | M_Records-> "Records" - | M_AC -> "AC" - | M_Expr-> "Expr" - | M_Triggers->"Triggers" - | M_Simplex->"Simplex" + | M_None -> "None" + | M_Typing -> "Typing" + | M_Sat -> "Sat" + | M_Match -> "Match" + | M_CC -> "CC" + | M_UF -> "UF" + | M_Arith -> "Arith" + | M_Arrays -> "Arrays" + | M_Sum -> "Sum" + | M_Records -> "Records" + | M_AC -> "AC" + | M_Expr -> "Expr" + | M_Triggers -> "Triggers" + | M_Simplex -> "Simplex" + | M_Ite -> "Ite" let string_of_ty_function f = match f with | F_add -> "add" diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli index 859f7db6b..1016d281b 100644 --- a/src/lib/util/timers.mli +++ b/src/lib/util/timers.mli @@ -43,6 +43,7 @@ type ty_module = | M_Expr | M_Triggers | M_Simplex + | M_Ite type ty_function = | F_add