From 90f98d5791a1c21a8804a26524df405d77c85ced Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Aug 2021 20:06:06 -0700
Subject: [PATCH] fix part of #5519

generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right.
---
 src/api/api_seq.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index d2b677330..ac65ab1f3 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -187,14 +187,18 @@ extern "C" {
         svector<char> buff;
         for (unsigned i = 0; i < str.length(); ++i) {
             unsigned ch = str[i];
-            if (ch >= 256) {
+            if (ch <= 32 || ch >= 127) {
                 buff.reset();
                 buffer.push_back('\\');
                 buffer.push_back('\\');  // possibly replace by native non-escaped version?
                 buffer.push_back('u');
                 buffer.push_back('{');
                 while (ch > 0) {
-                    buff.push_back('0' + (ch & 0xF));
+                    unsigned d = ch & 0xF;
+                    if (d < 10)
+                        buff.push_back('0' + d);
+                    else
+                        buff.push_back('a' + (d - 10));
                     ch /= 16;
                 }
                 for (unsigned j = buff.size(); j-- > 0; ) {