sig
  val identity : '-> 'a
  val print_pass : string -> '-> 'a
  val true_of_unit : unit -> bool
  val false_of_unit : unit -> bool
  val none_of_unit : unit -> 'a option
  val true_of_any : '-> bool
  val false_of_any : '-> bool
  val mk_dir : string -> unit
  val get : 'a option -> 'a
  val string_starts_with : string -> string -> bool
  val safe_hash_interleave : int -> int -> int -> int
  val ( @:: ) : 'a option -> 'a list -> 'a list
  val list_init : (int -> 'a) -> int -> 'a list
  val list_max : 'a list -> 'a
  val list_index : ('-> bool) -> 'a list -> int
  val list_indexes : 'a list -> 'a list -> int list
  val list_filter_nth : 'a list -> int list -> 'a list
  val list_extract_nth : 'a list -> int -> 'a * 'a list
  val chain_list : 'a list -> 'a list list
  val list_subtract : 'a list -> 'a list -> 'a list
  val list_uniq : 'a list -> 'a list
  val list_merge_uniq : ('-> '-> int) -> 'a list -> 'a list -> 'a list
  val list_inter_uniq : ('-> '-> int) -> 'a list -> 'a list -> 'a list
  val list_diff_uniq : ('-> '-> int) -> 'a list -> 'a list -> 'a list
  val list_subset_uniq : ('-> '-> int) -> 'a list -> 'a list -> bool
  val list_join :
    ('-> '-> bool) ->
    ('a * 'b) list -> ('a * 'b list) list -> ('a * 'b list) list
  val compare_pairs :
    ('-> '-> int) -> ('-> '-> int) -> 'a * '-> 'a * '-> int
  val compare_lists : ('-> '-> int) -> 'a list -> 'a list -> int
  val array_max : 'a array -> 'a
  module IntegerSet :
    sig
      type elt = int
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val map : (elt -> elt) -> t -> t
      val fold : (elt -> '-> 'a) -> t -> '-> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val find : elt -> t -> elt
      val of_list : elt list -> t
    end
  module IntegerHashtbl :
    sig
      type key = int
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> '-> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  val pp_print_arrayi :
    (Format.formatter -> int -> '-> unit) ->
    (unit, Format.formatter, unit) Pervasives.format ->
    Format.formatter -> 'a array -> unit
  val pp_print_list :
    (Format.formatter -> '-> unit) ->
    ('b, Format.formatter, unit) Pervasives.format ->
    Format.formatter -> 'a list -> unit
  val pp_print_listi :
    (Format.formatter -> int -> '-> unit) ->
    ('b, Format.formatter, unit) Pervasives.format ->
    Format.formatter -> 'a list -> unit
  val pp_print_list2i :
    (Format.formatter -> int -> '-> '-> unit) ->
    ('c, Format.formatter, unit) Pervasives.format ->
    Format.formatter -> 'a list -> 'b list -> unit
  val pp_print_option :
    (Format.formatter -> '-> unit) -> Format.formatter -> 'a option -> unit
  val pp_print_if_not_empty :
    (unit, Format.formatter, unit) Pervasives.format ->
    Format.formatter -> 'a list -> unit
  val string_of_t : (Format.formatter -> '-> unit) -> '-> string
  val width_of_string : string -> int
  val paren_string_of_string_list : string list -> string
  type log_level =
      L_off
    | L_fatal
    | L_error
    | L_warn
    | L_note
    | L_info
    | L_debug
    | L_trace
  val default_log_level : Lib.log_level
  val int_of_log_level : Lib.log_level -> int
  val log_level_of_int : int -> Lib.log_level
  val string_of_log_level : Lib.log_level -> string
  val log_ppf : Format.formatter Pervasives.ref
  val log_to_file : string -> unit
  val log_to_stdout : unit -> unit
  val set_log_level : Lib.log_level -> unit
  val get_log_level : unit -> Lib.log_level
  val output_on_level : Lib.log_level -> bool
  val ignore_or_fprintf :
    Lib.log_level ->
    Format.formatter -> ('a, Format.formatter, unit) Pervasives.format -> 'a
  val pp_print_banner : Format.formatter -> unit -> unit
  val pp_print_version : Format.formatter -> unit
  type kind_module =
      [ `BMC
      | `C2I
      | `Certif
      | `IC3
      | `IND
      | `IND2
      | `INVGEN
      | `INVGENINT
      | `INVGENINTOS
      | `INVGENOS
      | `INVGENREAL
      | `INVGENREALOS
      | `Interpreter
      | `Parser
      | `Supervisor ]
  exception TimeoutWall
  exception TimeoutVirtual
  exception Signal of int
  val string_of_signal : int -> string
  val pp_print_process_status :
    Format.formatter -> Unix.process_status -> unit
  val exception_on_signal : int -> 'a
  val pp_print_kind_module : Format.formatter -> Lib.kind_module -> unit
  val string_of_kind_module : Lib.kind_module -> string
  val int_of_kind_module : Lib.kind_module -> int
  val short_name_of_kind_module : Lib.kind_module -> string
  val kind_module_of_string : string -> Lib.kind_module
  val minisleep : float -> unit
  val find_on_path : string -> string
  type position
  val dummy_pos : Lib.position
  val compare_pos : Lib.position -> Lib.position -> int
  val is_dummy_pos : Lib.position -> bool
  val pp_print_position : Format.formatter -> Lib.position -> unit
  val pp_print_pos : Format.formatter -> Lib.position -> unit
  val file_row_col_of_pos : Lib.position -> string * int * int
  val pos_of_file_row_col : string * int * int -> Lib.position
  val position_of_lexing : Lexing.position -> Lib.position
  val print_backtrace : Format.formatter -> Printexc.raw_backtrace -> unit
  val extract_scope_name : string -> string * string list
  val create_dir : string -> unit
  val file_copy : string -> string -> unit
  val files_cat_open :
    ?add_prefix:(Format.formatter -> unit) ->
    string list -> string -> Unix.file_descr
  val syscall : string -> string
  val set_liberal_gc : unit -> unit
  val reset_gc_params : unit -> unit
  module Paths :
    sig val testgen : string val oracle : string val implem : string end
  module ReservedIds :
    sig
      val abs_ident_string : string
      val oracle_ident_string : string
      val instance_ident_string : string
      val init_flag_ident_string : string
      val all_req_ident_string : string
      val all_ens_ident_string : string
      val inst_ident_string : string
      val init_uf_string : string
      val trans_uf_string : string
      val index_ident_string : string
      val state_string : string
      val restart_string : string
      val state_selected_string : string
      val restart_selected_string : string
      val state_selected_next_string : string
      val restart_selected_next_string : string
      val handler_string : string
      val unless_string : string
      val init_flag_string : string
      val depth_input_string : string
      val max_depth_input_string : string
      val function_of_inputs : string
      val reserved_strings : string list
    end
  module ExitCodes :
    sig
      val unknown : int
      val unsafe : int
      val safe : int
      val error : int
      val kid_status : int
    end
  module Names :
    sig
      val contract_gen_file : string
      val contract_name : string list -> string
      val inv_log_file : string
      val inv_log_contract_name : string list -> string
    end
end