mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-29 20:59:01 +00:00
Code Activity

Fix Java API mkString to properly handle Unicode surrogate pairs (#7865)

Browse source 
* 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>
This commit is contained in:
Copilot 2025-09-11 11:13:31 -07:00 • committed by GitHub
parent 9196a3c369
commit 294f0578b0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/java/Context.java
View file

@ -2032,7 +2032,7 @@ public class Context implements AutoCloseable {
public SeqExpr<CharSort> mkString(String s) public SeqExpr<CharSort> mkString(String s)
{ {
StringBuilder buf = new StringBuilder(); 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); int code = s.codePointAt(i);
if (code <= 32 || 127 < code) if (code <= 32 || 127 < code)
buf.append(String.format("\\u{%x}", code)); buf.append(String.format("\\u{%x}", code));