sig
  module type Params =
    sig
      val produce_assignments : bool
      val produce_cores : bool
      val produce_proofs : bool
      val logic : TermLib.logic
      val id : int
    end
  module type Inst =
    sig
      module Conv : SMTExpr.Conv
      val delete_instance : unit -> unit
      val declare_sort : SMTExpr.sort -> SolverResponse.decl_response
      val declare_fun :
        string ->
        SMTExpr.sort list -> SMTExpr.sort -> SolverResponse.decl_response
      val define_fun :
        string ->
        SMTExpr.var list ->
        SMTExpr.sort -> SMTExpr.t -> SolverResponse.decl_response
      val assert_expr : SMTExpr.t -> SolverResponse.decl_response
      val push : int -> SolverResponse.decl_response
      val pop : int -> SolverResponse.decl_response
      val check_sat :
        ?timeout:int -> unit -> SolverResponse.check_sat_response
      val check_sat_assuming :
        SMTExpr.t list -> SolverResponse.check_sat_response
      val check_sat_assuming_supported : unit -> bool
      val get_value : SMTExpr.t list -> SolverResponse.get_value_response
      val get_model : unit -> SolverResponse.get_model_response
      val get_unsat_core : unit -> SolverResponse.get_unsat_core_response
      val execute_custom_command :
        string ->
        SMTExpr.custom_arg list -> int -> SolverResponse.custom_response
      val execute_custom_check_sat_command :
        string -> SolverResponse.check_sat_response
      val trace_comment : string -> unit
    end
  module type S = sig module Create : functor (P : Params-> Inst end
end