From 0d055b83eb6d1ed47805eb74d8e761efdecab027 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Dec 2021 09:04:18 -0800
Subject: [PATCH] update input for doxygen #5400

---
 src/api/java/Context.java | 13 ++++++-------
 src/api/z3_api.h          |  6 +++---
 2 files changed, 9 insertions(+), 10 deletions(-)

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)))
      */