sig
  type state
  val get_time : unit -> float
  val get_calls : unit -> int
  val clear : unit -> unit
  val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
  val check : ?profiling:bool -> unit -> unit
  val save_state : unit -> Smt.Solver.state
  val restore_state : Smt.Solver.state -> unit
  val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
end