From f91c3d9fd667a9f1d4adf94bb24fa9e2f2f94fbf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Aug 2021 20:36:38 -0700 Subject: [PATCH] round-tripping escapes, again #5519 --- src/api/api_seq.cpp | 2 +- src/api/python/z3/z3.py | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index ac65ab1f3..01e932353 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -190,7 +190,7 @@ extern "C" { if (ch <= 32 || ch >= 127) { buff.reset(); buffer.push_back('\\'); - buffer.push_back('\\'); // possibly replace by native non-escaped version? +// buffer.push_back('\\'); // possibly replace by native non-escaped version? buffer.push_back('u'); buffer.push_back('{'); while (ch > 0) { diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 3f0518650..5c0d5765a 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10706,12 +10706,11 @@ def is_string_value(a): """ return isinstance(a, SeqRef) and a.is_string_value() - def StringVal(s, ctx=None): """create a string expression""" - s = "".join(str(ch) if ord(ch) < 128 else "\\u{%x}" % (ord(ch)) for ch in s) + s = "".join(str(ch) if 32 <= ord(ch) and ord(ch) < 127 else "\\u{%x}" % (ord(ch)) for ch in s) ctx = _get_ctx(ctx) - return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx) + return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) def String(name, ctx=None):