sig
  type mc_engine_type = Absint | Armc | Cegar | Lart
  val mc_engine_names : (Option.Main.mc_engine_type * string) list
  type tc_engine_type = APInv_bwd | APInv_fwd | UPInv_bwd | UPInv_fwd
  val tc_engine_names : (Option.Main.tc_engine_type * string) list
  val mc_engine_opt : Option.Main.mc_engine_type Pervasives.ref
  val tc_engine_opt : Option.Main.tc_engine_type Pervasives.ref
  val k_opt : int Pervasives.ref
  val k_min_opt : int Pervasives.ref
  val k_max_opt : int Pervasives.ref
  val tc_discard_states_opt : bool Pervasives.ref
  val tc_validate_opt : bool Pervasives.ref
  val limit_opt : int Pervasives.ref
  val scm_source_file_opt : string option Pervasives.ref
  val scm_consistency_check_opt : bool Pervasives.ref
  val result_validation_opt : bool Pervasives.ref
  val show_statistics_opt : bool Pervasives.ref
  val mc_engine : unit -> Option.Main.mc_engine_type
  val tc_engine : unit -> Option.Main.tc_engine_type
  val k : unit -> int
  val k_min : unit -> int
  val k_max : unit -> int
  val tc_discard_states : unit -> bool
  val tc_validate : unit -> bool
  val limit : unit -> int
  val scm_source_file : unit -> string option
  val scm_consistency_check : unit -> bool
  val result_validation : unit -> bool
  val show_statistics : unit -> bool
  val control_arg_spec : unit -> (string * Arg.spec * string) list
  val verify_arg_spec : unit -> (string * Arg.spec * string) list
end