sig
  type t
  exception Unknown
  val create_instance :
    ?produce_assignments:bool ->
    ?produce_proofs:bool ->
    ?produce_cores:bool ->
    ?produce_interpolants:bool ->
    TermLib.logic -> Flags.Smt.solver -> SMTSolver.t
  val delete_instance : SMTSolver.t -> unit
  val destroy_all : unit -> unit
  val id_of_instance : SMTSolver.t -> int
  val declare_sort : SMTSolver.t -> Type.t -> unit
  val declare_fun : SMTSolver.t -> UfSymbol.t -> unit
  val define_fun : SMTSolver.t -> UfSymbol.t -> Var.t list -> Term.t -> unit
  val assert_expr : SMTSolver.t -> SMTExpr.t -> unit
  val assert_term : SMTSolver.t -> Term.t -> unit
  val assert_named_term : SMTSolver.t -> SMTExpr.t -> unit
  val assert_named_term_wr : SMTSolver.t -> SMTExpr.t -> string
  val push : ?n:int -> SMTSolver.t -> unit
  val pop : ?n:int -> SMTSolver.t -> unit
  val check_sat : ?timeout:int -> SMTSolver.t -> bool
  val get_model : SMTSolver.t -> Model.t
  val get_var_values :
    SMTSolver.t ->
    LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t ->
    Var.t list -> Model.t
  val get_unsat_core_of_names : SMTSolver.t -> Term.t list
  val get_unsat_core_lits : SMTSolver.t -> Term.t list
  val check_sat_assuming :
    SMTSolver.t ->
    (SMTSolver.t -> 'a) -> (SMTSolver.t -> 'a) -> Term.t list -> 'a
  val check_sat_and_get_term_values :
    SMTSolver.t ->
    (SMTSolver.t -> (Term.t * Term.t) list -> 'a) ->
    (SMTSolver.t -> 'a) -> Term.t list -> 'a
  val check_sat_assuming_and_get_term_values :
    SMTSolver.t ->
    (SMTSolver.t -> (Term.t * Term.t) list -> 'a) ->
    (SMTSolver.t -> 'a) -> Term.t list -> Term.t list -> 'a
  type ('a, 'b) sat_or_unsat = Sat of '| Unsat of 'b
  val check_sat_assuming_ab :
    SMTSolver.t ->
    (SMTSolver.t -> 'a) ->
    (SMTSolver.t -> 'b) -> Term.t list -> ('a, 'b) SMTSolver.sat_or_unsat
  val check_sat_assuming_tf : SMTSolver.t -> Term.t list -> bool
  val execute_custom_command :
    SMTSolver.t ->
    string ->
    SMTExpr.custom_arg list -> int -> SolverResponse.custom_response
  val execute_custom_check_sat_command :
    string -> SMTSolver.t -> SolverResponse.check_sat_response
  val converter : SMTSolver.t -> (module SMTExpr.Conv)
  val kind : SMTSolver.t -> Flags.Smt.solver
  val trace_comment : SMTSolver.t -> string -> unit
  val get_interpolants :
    SMTSolver.t -> SMTExpr.custom_arg list -> SMTExpr.t list
end