From 294f0578b06c5d0f5edafabe9dda7e983e945f82 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 11 Sep 2025 11:13:31 -0700 Subject: [PATCH] Fix Java API mkString to properly handle Unicode surrogate pairs (#7865) * Initial plan * Fix Java API mkString to properly handle surrogate pairs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/java/Context.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index f3efa632a..2350b52ae 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2032,7 +2032,7 @@ public class Context implements AutoCloseable { public SeqExpr mkString(String s) { StringBuilder buf = new StringBuilder(); - for (int i = 0; i < s.length(); ++i) { + for (int i = 0; i < s.length(); i += Character.charCount(s.codePointAt(i))) { int code = s.codePointAt(i); if (code <= 32 || 127 < code) buf.append(String.format("\\u{%x}", code));