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