sig
  val check_strategy : Smt_sig.S.check_strategy
  val get_time : unit -> float
  val get_calls : unit -> int
  val clear : unit -> unit
  val assume : id:int -> Smt_sig.S.Formula.t -> unit
  val check : unit -> unit
  val entails : Smt_sig.S.Formula.t -> bool
  val push : unit -> unit
  val pop : unit -> unit
end