sig
  type solver
  type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
  val string_of_status : Z3.Solver.status -> string
  module Statistics :
    sig
      type statistics
      module Entry :
        sig
          type statistics_entry
          val get_key : Z3.Solver.Statistics.Entry.statistics_entry -> string
          val get_int : Z3.Solver.Statistics.Entry.statistics_entry -> int
          val get_float :
            Z3.Solver.Statistics.Entry.statistics_entry -> float
          val is_int : Z3.Solver.Statistics.Entry.statistics_entry -> bool
          val is_float : Z3.Solver.Statistics.Entry.statistics_entry -> bool
          val to_string_value :
            Z3.Solver.Statistics.Entry.statistics_entry -> string
          val to_string :
            Z3.Solver.Statistics.Entry.statistics_entry -> string
        end
      val to_string : Z3.Solver.Statistics.statistics -> string
      val get_size : Z3.Solver.Statistics.statistics -> int
      val get_entries :
        Z3.Solver.Statistics.statistics ->
        Z3.Solver.Statistics.Entry.statistics_entry list
      val get_keys : Z3.Solver.Statistics.statistics -> string list
      val get :
        Z3.Solver.Statistics.statistics ->
        string -> Z3.Solver.Statistics.Entry.statistics_entry option
    end
  val get_help : Z3.Solver.solver -> string
  val set_parameters : Z3.Solver.solver -> Z3.Params.params -> unit
  val get_param_descrs :
    Z3.Solver.solver -> Z3.Params.ParamDescrs.param_descrs
  val get_num_scopes : Z3.Solver.solver -> int
  val push : Z3.Solver.solver -> unit
  val pop : Z3.Solver.solver -> int -> unit
  val reset : Z3.Solver.solver -> unit
  val add : Z3.Solver.solver -> Z3.Expr.expr list -> unit
  val assert_and_track_l :
    Z3.Solver.solver -> Z3.Expr.expr list -> Z3.Expr.expr list -> unit
  val assert_and_track :
    Z3.Solver.solver -> Z3.Expr.expr -> Z3.Expr.expr -> unit
  val get_num_assertions : Z3.Solver.solver -> int
  val get_assertions : Z3.Solver.solver -> Z3.Expr.expr list
  val check : Z3.Solver.solver -> Z3.Expr.expr list -> Z3.Solver.status
  val get_model : Z3.Solver.solver -> Z3.Model.model option
  val get_proof : Z3.Solver.solver -> Z3.Expr.expr option
  val get_unsat_core : Z3.Solver.solver -> Z3.AST.ast list
  val get_reason_unknown : Z3.Solver.solver -> string
  val get_statistics : Z3.Solver.solver -> Z3.Solver.Statistics.statistics
  val mk_solver : Z3.context -> Z3.Symbol.symbol option -> Z3.Solver.solver
  val mk_solver_s : Z3.context -> string -> Z3.Solver.solver
  val mk_simple_solver : Z3.context -> Z3.Solver.solver
  val mk_solver_t : Z3.context -> Z3.Tactic.tactic -> Z3.Solver.solver
  val to_string : Z3.Solver.solver -> string
end