sig
  type trace = NoTrace | AltErgoTr | WhyTr | WhyInst
  type viz_prog = Dot | Sfdp
  type solver = AltErgo | Z3
  val file : string
  val cin : Pervasives.in_channel
  val max_proc : int
  val type_only : bool
  val maxrounds : int
  val maxnodes : int
  val only_forward : bool
  val gen_inv : bool
  val forward_inv : int
  val enumerative : int
  val localized : bool
  val lazyinv : bool
  val refine : bool
  val stateless : bool
  val do_brab : bool
  val brab_up_to : bool
  val murphi : bool
  val murphi_uopts : string
  val mu_cmd : string
  val mu_opts : string
  val cpp_cmd : string
  val limit_forward_depth : bool
  val forward_depth : int
  val max_forward : int
  val max_cands : int
  val candidate_heuristic : int
  val forward_sym : bool
  val abstr_num : bool
  val num_range : int * int
  val post_strategy : int
  val delete : bool
  val simpl_by_uc : bool
  val noqe : bool
  val bitsolver : bool
  val enumsolver : bool
  val refine_universal : bool
  val cores : int
  val mode : string
  val debug : bool
  val dot : bool
  val dot_level : int
  val dot_prog : Options.viz_prog
  val dot_colors : int
  val quiet : bool
  val verbose : int
  val nocolor : bool
  val smt_solver : Options.solver
  val debug_smt : bool
  val dmcmt : bool
  val profiling : bool
  val size_proc : int Pervasives.ref
  val subtyping : bool
  val notyping : bool
  val trace : Options.trace
  val out_trace : string
  val js_mode : unit -> bool
  val set_js_mode : bool -> unit
end