sig
  val mk_interpolant : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_interpolation_context : (string * string) list -> Z3.context
  val get_interpolant :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Params.params -> Z3.Expr.expr list
  val compute_interpolant :
    Z3.context ->
    Z3.Expr.expr ->
    Z3.Params.params ->
    Z3enums.lbool * Z3.Expr.expr list option * Z3.Model.model option
  val get_interpolation_profile : Z3.context -> string
  val read_interpolation_problem :
    Z3.context -> string -> Z3.Expr.expr list * int list * Z3.Expr.expr list
  val check_interpolant :
    Z3.context ->
    int ->
    Z3.Expr.expr list ->
    int list -> Z3.Expr.expr list -> int -> Z3.Expr.expr list -> unit
  val write_interpolation_problem :
    Z3.context ->
    int ->
    Z3.Expr.expr list ->
    int list -> string -> int -> Z3.Expr.expr list -> unit
end