From 6013d5da471edfca38ff2a08d3ff2139147ae9bc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Jan 2022 14:05:06 -0800
Subject: [PATCH] #5755

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/java/Context.java | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 0a597a6ce..b22bedef7 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2016,7 +2016,15 @@ public class Context implements AutoCloseable {
      */
     public SeqExpr<CharSort> mkString(String s)
     {
-        return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), s));
+        StringBuilder buf = new StringBuilder();
+        for (int i = 0; i < s.length(); ++i) {
+	    int code = s.codePointAt(i);
+	    if (code <= 32 || 127 < code) 
+	        buf.append(String.format("\\u{%x}", code));
+	    else
+	        buf.append(s.charAt(i));
+        }
+        return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), buf.toString()));
     }
 
     /**