sig
  type solver
  type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
  val string_of_status : Z3.Solver.status -> string
  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.Expr.expr list
  val get_reason_unknown : Z3.Solver.solver -> string
  val get_statistics : Z3.Solver.solver -> Z3.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 add_simplifier :
    Z3.context ->
    Z3.Solver.solver -> Z3.Simplifier.simplifier -> Z3.Solver.solver
  val translate : Z3.Solver.solver -> Z3.context -> Z3.Solver.solver
  val to_string : Z3.Solver.solver -> string
  val interrupt : Z3.context -> Z3.Solver.solver -> unit
end