sig
  type 'a t
  val add : 'a SrkZ3.Solver.t -> 'a Syntax.formula list -> unit
  val push : 'a SrkZ3.Solver.t -> unit
  val pop : 'a SrkZ3.Solver.t -> int -> unit
  val reset : 'a SrkZ3.Solver.t -> unit
  val check :
    'a SrkZ3.Solver.t ->
    'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
  val to_string : 'a SrkZ3.Solver.t -> string
  val get_model :
    ?symbols:Syntax.symbol list ->
    'a SrkZ3.Solver.t ->
    [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
  val get_concrete_model :
    'a SrkZ3.Solver.t ->
    Syntax.symbol list ->
    [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
  val get_unsat_core :
    'a SrkZ3.Solver.t ->
    'a Syntax.formula list ->
    [ `Sat | `Unknown | `Unsat of 'a Syntax.formula list ]
end