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