diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py
index a944f2c65..a1a9e64bd 100644
--- a/doc/mk_api_doc.py
+++ b/doc/mk_api_doc.py
@@ -226,12 +226,14 @@ try:
website_dox_substitutions = {}
bullet_point_prefix='\n - '
if Z3PY_ENABLED:
+ print("Python documentation enabled")
website_dox_substitutions['PYTHON_API'] = (
'{prefix}Python API '
'(also available in pydoc format)'
).format(
prefix=bullet_point_prefix)
else:
+ print("Python documentation disabled")
website_dox_substitutions['PYTHON_API'] = ''
if DOTNET_ENABLED:
website_dox_substitutions['DOTNET_API'] = (
@@ -250,7 +252,7 @@ try:
website_dox_substitutions['JAVA_API'] = ''
if ML_ENABLED:
website_dox_substitutions['OCAML_API'] = (
- 'ML/OCaml API'
+ '{prefix}ML/OCaml API'
).format(
prefix=bullet_point_prefix)
else:
@@ -316,7 +318,7 @@ try:
if ML_ENABLED:
ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml')
mk_dir(ml_output_dir)
- if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, doc_path('../src/api/ml/z3enums.mli'), doc_path('../src/api/ml/z3.mli')]) != 0:
+ if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '%s/api/ml/z3enums.mli' % BUILD_DIR, '%s/api/ml/z3.mli' % BUILD_DIR]) != 0:
print("ERROR: ocamldoc failed.")
exit(1)
print("Generated ML/OCaml documentation.")
@@ -326,3 +328,4 @@ except Exception:
exctype, value = sys.exc_info()[:2]
print("ERROR: failed to generate documentation: %s" % value)
exit(1)
+
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 9f4cd9cd9..80923a0c7 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3443,12 +3443,10 @@ sig
(** Parse the given string using the SMT-LIB2 parser.
- {!parse_smtlib_string}
@return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
- (** Parse the given file using the SMT-LIB2 parser.
- {!parse_smtlib2_string} *)
+ (** Parse the given file using the SMT-LIB2 parser. *)
val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
end
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 064476b9b..007bc3ab6 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1331,7 +1331,7 @@ typedef enum {
- Z3_IOB: Index out of bounds.
- Z3_INVALID_ARG: Invalid argument was provided.
- Z3_PARSER_ERROR: An error occurred when parsing a string or file.
- - Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
+ - Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
- Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
- Z3_MEMOUT_FAIL: A memory allocation failure was encountered.
- Z3_FILE_ACCESS_ERRROR: A file could not be accessed.