sig
  type int_item
  type float_item
  type int_list_item
  type stat_item
  val set : int -> Stat.int_item -> unit
  val set_float : float -> Stat.float_item -> unit
  val set_int_list : int list -> Stat.int_list_item -> unit
  val incr : ?by:int -> Stat.int_item -> unit
  val incr_last : ?by:int -> Stat.int_list_item -> unit
  val append : int -> Stat.int_list_item -> unit
  val reset : Stat.int_item -> unit
  val reset_float : Stat.float_item -> unit
  val reset_int_list : Stat.int_list_item -> unit
  val get : Stat.int_item -> int
  val get_float : Stat.float_item -> float
  val get_int_list : Stat.int_list_item -> int list
  val start_timer : Stat.float_item -> unit
  val record_time : Stat.float_item -> unit
  val unpause_time : Stat.float_item -> unit
  val update_time : Stat.float_item -> unit
  val time_fun : Stat.float_item -> (unit -> 'a) -> 'a
  val pp_print_stats : Format.formatter -> Stat.stat_item list -> unit
  val pp_print_stats_xml : Format.formatter -> Stat.stat_item list -> unit
  val pp_print_stats_json : Format.formatter -> Stat.stat_item list -> unit
  val bmc_k : Stat.int_item
  val bmc_total_time : Stat.float_item
  val bmc_stop_timers : unit -> unit
  val bmc_stats_title : string
  val bmc_stats : Stat.stat_item list
  val pp_print_bmc_stats : Format.formatter -> unit
  val ind_k : Stat.int_item
  val ind_compress_equal_mod_input : Stat.int_item
  val ind_compress_same_successors : Stat.int_item
  val ind_compress_same_predecessors : Stat.int_item
  val ind_restarts : Stat.int_item
  val ind_lazy_invariants_count : Stat.int_item
  val ind_lazy_invariants_time : Stat.float_item
  val ind_total_time : Stat.float_item
  val ind_stop_timers : unit -> unit
  val ind_stats_title : string
  val ind_stats : Stat.stat_item list
  val pp_print_ind_stats : Format.formatter -> unit
  val ic3_k : Stat.int_item
  val ic3_restarts : Stat.int_item
  val ic3_frame_sizes : Stat.int_list_item
  val ic3_fwd_propagated : Stat.int_item
  val ic3_fwd_gen_propagated : Stat.int_item
  val ic3_fwd_subsumed : Stat.int_item
  val ic3_back_subsumed : Stat.int_item
  val ic3_fwd_fixpoint : Stat.int_item
  val ic3_inductive_blocking_clauses : Stat.int_item
  val ic3_total_time : Stat.float_item
  val ic3_fwd_prop_time : Stat.float_item
  val ic3_strengthen_time : Stat.float_item
  val ic3_find_cex_time : Stat.float_item
  val ic3_ind_gen_time : Stat.float_item
  val ic3_generalize_time : Stat.float_item
  val ic3_inductive_check_time : Stat.float_item
  val ic3_activation_literals : Stat.int_item
  val ic3_stale_activation_literals : Stat.int_item
  val ic3_stop_timers : unit -> unit
  val ic3_stats_title : string
  val ic3_stats : Stat.stat_item list
  val pp_print_ic3_stats : Format.formatter -> unit
  val ic3ia_refinements : Stat.int_list_item
  val ic3ia_refinements_end : Stat.int_list_item
  val ic3ia_num_simulations : Stat.int_item
  val ic3ia_interpolation_time : Stat.float_item
  val ic3ia_stats_title : string
  val ic3ia_stats : Stat.stat_item list
  val pp_print_ic3ia_stats : Format.formatter -> unit
  val invgengraph_os_k : Stat.int_item
  val invgengraph_os_candidate_term_count : Stat.int_item
  val invgengraph_os_invariant_count : Stat.int_item
  val invgengraph_os_implication_count : Stat.int_item
  val invgengraph_os_graph_rewriting_time : Stat.float_item
  val invgengraph_os_total_time : Stat.float_item
  val invgengraph_os_stats_title : string
  val invgengraph_os_stats : Stat.stat_item list
  val invgengraph_os_stop_timers : unit -> unit
  val pp_print_invgengraph_os_stats : Format.formatter -> unit
  val invgengraph_ts_k : Stat.int_item
  val invgengraph_ts_candidate_term_count : Stat.int_item
  val invgengraph_ts_invariant_count : Stat.int_item
  val invgengraph_ts_implication_count : Stat.int_item
  val invgengraph_ts_graph_rewriting_time : Stat.float_item
  val invgengraph_ts_total_time : Stat.float_item
  val invgengraph_ts_stats_title : string
  val invgengraph_ts_stats : Stat.stat_item list
  val invgengraph_ts_stop_timers : unit -> unit
  val pp_print_invgengraph_ts_stats : Format.formatter -> unit
  val c2i_str_invs : Stat.int_item
  val c2i_zero_cost : Stat.int_item
  val c2i_moves : Stat.int_item
  val c2i_move_time : Stat.float_item
  val c2i_query_time : Stat.float_item
  val c2i_model_comp_time : Stat.float_item
  val c2i_total_time : Stat.float_item
  val c2i_stats_title : string
  val c2i_stats : Stat.stat_item list
  val c2i_stop_timers : unit -> unit
  val pp_print_c2i_stats : Format.formatter -> unit
  val testgen_testcases : Stat.int_item
  val testgen_deadlocks : Stat.int_item
  val testgen_restarts : Stat.int_item
  val testgen_forward_time : Stat.float_item
  val testgen_backward_time : Stat.float_item
  val testgen_enumerate_time : Stat.float_item
  val testgen_total_time : Stat.float_item
  val testgen_stats_title : string
  val testgen_stats : Stat.stat_item list
  val testgen_stop_timers : unit -> unit
  val pp_print_testgen_stats : Format.formatter -> unit
  val smt_check_sat_time : Stat.float_item
  val smt_get_value_time : Stat.float_item
  val smt_get_unsat_core_time : Stat.float_item
  val smt_stop_timers : unit -> unit
  val smt_stats_title : string
  val smt_stats : Stat.stat_item list
  val pp_print_smt_stats : Format.formatter -> unit
  val certif_gen_time : Stat.float_item
  val certif_min_time : Stat.float_item
  val certif_frontend_time : Stat.float_item
  val certif_cvc4_time : Stat.float_item
  val certif_k : Stat.int_item
  val certif_size : Stat.int_item
  val certif_old_k : Stat.int_item
  val certif_old_size : Stat.int_item
  val certif_stop_timers : unit -> unit
  val certif_stats_title : string
  val certif_stats : Stat.stat_item list
  val pp_print_certif_stats : Format.formatter -> unit
  val total_time : Stat.float_item
  val analysis_time : Stat.float_item
  val clause_of_term_time : Stat.float_item
  val smtexpr_of_term_time : Stat.float_item
  val term_of_smtexpr_time : Stat.float_item
  val misc_stop_timers : unit -> unit
  val misc_stats_title : string
  val misc_stats : Stat.stat_item list
  val pp_print_misc_stats : Format.formatter -> unit
end