diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index ca7c860db0e..e1a6325dcd4 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -198,7 +198,7 @@ extern "C" {
         svector<char> buff;
         for (unsigned i = 0; i < str.length(); ++i) {
             unsigned ch = str[i];
-            if (ch <= 32 || ch >= 127 || (ch == '\\' && i + 1 < str.length() && str[i+1] == 'u')) {
+            if (ch == 0 || ch >= 256 || (ch == '\\' && i + 1 < str.length() && str[i+1] == 'u')) {
                 buff.reset();
                 buffer.push_back('\\');
                 buffer.push_back('u');
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index f81bcb6f8d1..d2544361721 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1120,12 +1120,9 @@ namespace z3 {
         std::u32string get_u32string() const {
             assert(is_string_value());
             unsigned n = Z3_get_string_length(ctx(), m_ast);
-            std::vector<unsigned> buffer;
-            buffer.resize(n);
-            Z3_get_string_contents(ctx(), m_ast, n, buffer.data());
             std::u32string s;
-            for (auto ch : buffer)
-                s.push_back(ch);
+            s.resize(n);
+            Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
             return s;
         }
 
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 7d252fd2646..a1b37cc8b57 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3480,6 +3480,11 @@ 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.
+
        def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING)))
      */
     Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
@@ -3487,7 +3492,8 @@ 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 unescaped.
+       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.
 
        def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING)))
      */
@@ -3511,6 +3517,7 @@ extern "C" {
 
     /**
        \brief Retrieve the string constant stored in \c s.
+       Characters outside the basic printiable ASCII range are escaped.
 
        \pre  Z3_is_string(c, s)
 
@@ -3520,6 +3527,8 @@ extern "C" {
 
     /**
        \brief Retrieve the string constant stored in \c s. The string can contain escape sequences.
+       Characters in the range 1 to 255 are literal. 
+       Characters in the range 0, and 256 above are escaped.
 
        \pre  Z3_is_string(c, s)