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