mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

round-tripping escapes, again #5519

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-31 20:36:38 -07:00
parent 90f98d5791
commit f91c3d9fd6
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_seq.cpp
View file

@ -190,7 +190,7 @@ extern "C" {
if (ch <= 32 || ch >= 127) { if (ch <= 32 || ch >= 127) {
buff.reset(); buff.reset();
buffer.push_back('\\'); 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('u');
buffer.push_back('{'); buffer.push_back('{');
while (ch > 0) { while (ch > 0) {

5
src/api/python/z3/z3.py
View file

@ -10706,12 +10706,11 @@ def is_string_value(a):
""" """
return isinstance(a, SeqRef) and a.is_string_value() return isinstance(a, SeqRef) and a.is_string_value()
def StringVal(s, ctx=None): def StringVal(s, ctx=None):
"""create a string expression""" """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) 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): def String(name, ctx=None):