val solver_time : float refval solver_count : int refval pp_statistics : Format.formatter -> t -> unitval create : ?params:Smtml.Params.t -> ?logic:Smtml.Ty.logic -> unit -> tval interrupt : t -> unitval push : t -> unitval pop : t -> int -> unitval reset : t -> unitval add : t -> Smtml.Expr.t list -> unitval get_assertions : t -> Smtml.Expr.t listval check : t -> Smtml.Expr.t list -> [ `Sat | `Unsat | `Unknown ]val get_value : t -> Smtml.Expr.t -> Smtml.Expr.tval model : ?symbols:Smtml.Symbol.t list -> t -> Smtml.Model.t option