sig
  val benchmark_to_smtstring :
    Z3.context ->
    string ->
    string -> string -> string -> Z3.Expr.expr list -> Z3.Expr.expr -> string
  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.AST.ASTVector.ast_vector
  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.AST.ASTVector.ast_vector
end