diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 6b49e9e27..9fcdfb1b5 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1717,9 +1717,8 @@ public class Context implements AutoCloseable { * {@code [domain -> range]}, and {@code i} must have the sort * {@code domain}. The sort of the result is {@code range}. * - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkStore - **/ public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i) { @@ -1740,7 +1739,7 @@ public class Context implements AutoCloseable { * {@code [domains -> range]}, and {@code args} must have the sorts * {@code domains}. The sort of the result is {@code range}. * - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkStore **/ public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args) @@ -1764,7 +1763,7 @@ public class Context implements AutoCloseable { * {@code select}) on all indices except for {@code i}, where it * maps to {@code v} (and the {@code select} of {@code a} * with respect to {@code i} may be a different value). - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect **/ @@ -1789,7 +1788,7 @@ public class Context implements AutoCloseable { * {@code select}) on all indices except for {@code args}, where it * maps to {@code v} (and the {@code select} of {@code a} * with respect to {@code args} may be a different value). - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect **/ @@ -1807,7 +1806,7 @@ public class Context implements AutoCloseable { * Remarks: The resulting term is an array, such * that a {@code select} on an arbitrary index produces the value * {@code v}. - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect * **/ @@ -1827,7 +1826,7 @@ public class Context implements AutoCloseable { * {@code f} must have type {@code range_1 .. range_n -> range}. * {@code v} must have sort range. The sort of the result is * {@code [domain_i -> range]}. - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect * @see #mkStore diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2fe9a96e7..a63008051 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3488,8 +3488,8 @@ extern "C" { \brief Create a string constant out of the string that is passed in The string may contain escape encoding for non-printable characters or characters outside of the basic printable ASCII range. For example, - the escape encoding \u{0} represents the character 0 and the encoding - \u{100} represents the character 256. + the escape encoding \\u{0} represents the character 0 and the encoding + \\u{100} represents the character 256. def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING))) */ @@ -3499,7 +3499,7 @@ extern "C" { \brief Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is treated as if it is unescaped so a sequence - of characters \u{0} is treated as 5 characters and not the character 0. + of characters \\u{0} is treated as 5 characters and not the character 0. def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING))) */