sig
  val input_file : unit -> string
  val all_input_files : unit -> string list
  val clear_input_files : unit -> unit
  val add_input_file : string -> unit
  val lus_main : unit -> string option
  type input_format = [ `Horn | `Lustre | `Native ]
  val input_format : unit -> Flags.input_format
  val output_dir : unit -> string
  val log_invs : unit -> bool
  val debug : unit -> string list
  val debug_log : unit -> string option
  val log_level : unit -> Lib.log_level
  val log_format_xml : unit -> bool
  val timeout_wall : unit -> float
  val timeout_analysis : unit -> float
  type enable = Lib.kind_module list
  val enabled : unit -> Flags.enable
  val invgen_enabled : unit -> Flags.enable
  val disable : Lib.kind_module -> unit
  val modular : unit -> bool
  val lus_strict : unit -> bool
  val lus_compile : unit -> bool
  val color : unit -> bool
  val weakhcons : unit -> bool
  module Smt :
    sig
      type logic = [ `Logic of string | `None | `detect ]
      val logic : unit -> Flags.Smt.logic
      type solver =
          [ `CVC4_SMTLIB
          | `Yices_SMTLIB
          | `Yices_native
          | `Z3_SMTLIB
          | `detect ]
      val set_solver : Flags.Smt.solver -> unit
      val solver : unit -> Flags.Smt.solver
      val check_sat_assume : unit -> bool
      val short_names : unit -> bool
      val set_short_names : bool -> unit
      val z3_bin : unit -> string
      val cvc4_bin : unit -> string
      val yices_bin : unit -> string
      val yices2smt2_bin : unit -> string
      val set_trace : bool -> unit
      val trace : unit -> bool
      val trace_dir : unit -> string
    end
  module BmcKind :
    sig
      val max : unit -> int
      val check_unroll : unit -> bool
      val print_cex : unit -> bool
      val compress : unit -> bool
      val compress_equal : unit -> bool
      val compress_same_succ : unit -> bool
      val compress_same_pred : unit -> bool
      val lazy_invariants : unit -> bool
    end
  module IC3 :
    sig
      type qe = [ `Cooper | `Z3 | `Z3_impl | `Z3_impl2 ]
      val qe : unit -> Flags.IC3.qe
      val set_qe : Flags.IC3.qe -> unit
      val check_inductive : unit -> bool
      val print_to_file : unit -> string option
      val inductively_generalize : unit -> int
      val block_in_future : unit -> bool
      val block_in_future_first : unit -> bool
      val fwd_prop_non_gen : unit -> bool
      val fwd_prop_ind_gen : unit -> bool
      val fwd_prop_subsume : unit -> bool
      val use_invgen : unit -> bool
      type abstr = [ `IA | `None ]
      val abstr : unit -> Flags.IC3.abstr
      type extract = [ `First | `Vars ]
      val extract : unit -> Flags.IC3.extract
    end
  module QE :
    sig
      val order_var_by_elim : unit -> bool
      val general_lbound : unit -> bool
    end
  module Contracts :
    sig
      val compositional : unit -> bool
      val translate_contracts : unit -> string option
      val check_modes : unit -> bool
      val check_implem : unit -> bool
      val contract_gen : unit -> bool
      val contract_gen_depth : unit -> int
      val refinement : unit -> bool
    end
  module Certif :
    sig
      type mink = [ `Auto | `Bwd | `Dicho | `FrontierDicho | `Fwd | `No ]
      type mininvs = [ `Easy | `Hard | `HardOnly | `Medium | `MediumOnly ]
      val certif : unit -> bool
      val proof : unit -> bool
      val abstr : unit -> bool
      val log_trust : unit -> bool
      val mink : unit -> Flags.Certif.mink
      val mininvs : unit -> Flags.Certif.mininvs
      val jkind_bin : unit -> string
      val only_user_candidates : unit -> bool
    end
  module Arrays :
    sig
      val smt : unit -> bool
      val inline : unit -> bool
      val recdef : unit -> bool
      val var_size : unit -> bool
    end
  module Testgen :
    sig
      val active : unit -> bool
      val graph_only : unit -> bool
      val len : unit -> int
    end
  module Invgen :
    sig
      val prune_trivial : unit -> bool
      val set_max_depth : int option -> unit
      val max_depth : unit -> int option
      val max_succ : unit -> int
      val lift_candidates : unit -> bool
      val top_only : unit -> bool
      val all_out : unit -> bool
      val mine_trans : unit -> bool
      val two_state : unit -> bool
      val bool_eq_only : unit -> bool
      val arith_eq_only : unit -> bool
      val renice : unit -> int
    end
  module C2I :
    sig
      val dnf_size : unit -> int
      val int_cube_size : unit -> int
      val real_cube_size : unit -> int
      val modes : unit -> bool
    end
  module Interpreter :
    sig val input_file : unit -> string val steps : unit -> int end
  val subdir_for : string list -> string
end