diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 46fe5bd6d..ce305bb4e 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1975,56 +1975,6 @@ struct
       (List.length assumptions) assumptions
       formula
 
-  let parse_smtlib_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
-    let csn = List.length sort_names in
-    let cs = List.length sorts in
-    let cdn = List.length decl_names in
-    let cd = List.length decls in
-    if (csn <> cs || cdn <> cd) then
-      raise (Error "Argument size mismatch")
-    else
-      Z3native.parse_smtlib_string ctx str
-        cs sort_names sorts cd decl_names decls
-
-  let parse_smtlib_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
-    let csn = (List.length sort_names) in
-    let cs = (List.length sorts) in
-    let cdn = (List.length decl_names) in
-    let cd = (List.length decls) in
-    if (csn <> cs || cdn <> cd) then
-      raise (Error "Argument size mismatch")
-    else
-      Z3native.parse_smtlib_file ctx file_name
-        cs sort_names sorts cd decl_names decls
-
-  let get_num_smtlib_formulas (ctx:context) = Z3native.get_smtlib_num_formulas ctx
-
-  let get_smtlib_formulas (ctx:context) =
-    let n = get_num_smtlib_formulas ctx in
-    let f i = Z3native.get_smtlib_formula ctx i in
-    mk_list f n
-
-  let get_num_smtlib_assumptions (ctx:context) = Z3native.get_smtlib_num_assumptions ctx
-
-  let get_smtlib_assumptions (ctx:context) =
-    let n = get_num_smtlib_assumptions ctx in
-    let f i = Z3native.get_smtlib_assumption ctx i in
-    mk_list f n
-
-  let get_num_smtlib_decls (ctx:context) = Z3native.get_smtlib_num_decls ctx
-
-  let get_smtlib_decls (ctx:context) =
-    let n = get_num_smtlib_decls ctx in
-    let f i = Z3native.get_smtlib_decl ctx i in
-    mk_list f n
-
-  let get_num_smtlib_sorts (ctx:context)  = Z3native.get_smtlib_num_sorts ctx
-
-  let get_smtlib_sorts (ctx:context) =
-    let n = get_num_smtlib_sorts ctx in
-    let f i = Z3native.get_smtlib_sort ctx i in
-    mk_list f n
-
   let parse_smtlib2_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
     let csn = List.length sort_names in
     let cs = List.length sorts in
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 4f10b275a..9f4cd9cd9 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3441,43 +3441,6 @@ sig
       @return A string representation of the benchmark. *)
   val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string
 
-  (** Parse the given string using the SMT-LIB parser.
-
-      The symbol table of the parser can be initialized using the given sorts and declarations.
-      The symbols in the arrays in the third and fifth argument
-      don't need to match the names of the sorts and declarations in the arrays in the fourth
-      and sixth argument. This is a useful feature since we can use arbitrary names to
-      reference sorts and declarations. *)
-  val parse_smtlib_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
-
-  (** Parse the given file using the SMT-LIB parser.
-      {!parse_smtlib_string} *)
-  val parse_smtlib_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
-
-  (** The number of SMTLIB formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_num_smtlib_formulas : context -> int
-
-  (** The formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_smtlib_formulas : context -> Expr.expr list
-
-  (** The number of SMTLIB assumptions parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_num_smtlib_assumptions : context -> int
-
-  (** The assumptions parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_smtlib_assumptions : context -> Expr.expr list
-
-  (** The number of SMTLIB declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_num_smtlib_decls : context -> int
-
-  (** The declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_smtlib_decls : context -> FuncDecl.func_decl list
-
-  (** The number of SMTLIB sorts parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_num_smtlib_sorts : context -> int
-
-  (** The sort declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
-  val get_smtlib_sorts : context -> Sort.sort list
-
   (** Parse the given string using the SMT-LIB2 parser.
 
       {!parse_smtlib_string}