sig
  val benchmark_to_smtstring :
    Z3.context ->
    string ->
    string -> string -> string -> Z3.Expr.expr list -> Z3.Expr.expr -> string
  val parse_smtlib_string :
    Z3.context ->
    string ->
    Z3.Symbol.symbol list ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> unit
  val parse_smtlib_file :
    Z3.context ->
    string ->
    Z3.Symbol.symbol list ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> unit
  val get_num_smtlib_formulas : Z3.context -> int
  val get_smtlib_formulas : Z3.context -> Z3.Expr.expr list
  val get_num_smtlib_assumptions : Z3.context -> int
  val get_smtlib_assumptions : Z3.context -> Z3.Expr.expr list
  val get_num_smtlib_decls : Z3.context -> int
  val get_smtlib_decls : Z3.context -> Z3.FuncDecl.func_decl list
  val get_num_smtlib_sorts : Z3.context -> int
  val get_smtlib_sorts : Z3.context -> Z3.Sort.sort list
  val parse_smtlib2_string :
    Z3.context ->
    string ->
    Z3.Symbol.symbol list ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> Z3.Expr.expr
  val parse_smtlib2_file :
    Z3.context ->
    string ->
    Z3.Symbol.symbol list ->
    Z3.Sort.sort list ->
    Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> Z3.Expr.expr
end