sig
  module type SMTLIBSolverDriver =
    sig
      val cmd_line :
        TermLib.logic -> bool -> bool -> bool -> bool -> string array
      val check_sat_limited_cmd : int -> string
      val check_sat_assuming_supported : unit -> bool
      val check_sat_assuming_cmd : unit -> string
      val headers : unit -> string list
      val prelude : string list
      val trace_extension : string
      val comment_delims : string * string
      val interpr_type : Type.t -> Type.t
      val pp_print_sort : Format.formatter -> Type.t -> unit
      val string_of_sort : Type.t -> string
      val string_of_logic : TermLib.logic -> string
      val pp_print_logic : Format.formatter -> TermLib.logic -> unit
      val pp_print_symbol :
        ?arity:int -> Format.formatter -> Symbol.t -> unit
      val string_of_symbol : ?arity:int -> Symbol.t -> string
      val pp_print_expr : Format.formatter -> Term.t -> unit
      val print_expr : Term.t -> unit
      val string_of_expr : Term.t -> string
      val s_define_fun : HString.t
      val expr_of_string_sexpr : HStringSExpr.t -> Term.t
      val expr_or_lambda_of_string_sexpr :
        HStringSExpr.t -> HString.t * Model.value
    end
  module Make : functor (D : SMTLIBSolverDriver-> SolverSig.S
end