sig
  type error_response = [ `Error of string ]
  type no_response = [ `NoResponse ]
  type decl_response =
      [ `Error of string | `NoResponse | `Success | `Unsupported ]
  type check_sat_response = [ `Error of string | `Sat | `Unknown | `Unsat ]
  type get_value_response =
      [ `Error of string | `Values of (Term.t * Term.t) list ]
  type get_model_response =
      [ `Error of string | `Model of (UfSymbol.t * Model.value) list ]
  type get_unsat_core_response =
      [ `Error of string | `Unsat_core of string list ]
  type custom_response =
      [ `Custom of HStringSExpr.t list | `Error of string ]
  type response =
      [ `Custom of HStringSExpr.t list
      | `Error of string
      | `Model of (UfSymbol.t * Model.value) list
      | `NoResponse
      | `Sat
      | `Success
      | `Unknown
      | `Unsat
      | `Unsat_core of string list
      | `Unsupported
      | `Values of (Term.t * Term.t) list ]
  val pp_print_response : Format.formatter -> SolverResponse.response -> unit
end