-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unable to modify string encoding #6490
Comments
Also, note that, in the block that presumably handles |
the escape characters are just \u{}. I don't have different escape characters for ascii. The character range for ascii is still 256.
|
Thank you for your reply @NikolajBjorner . When using either:
or
and adding the following to
the return is always "UNICODE". Also, in previous versions of Z3, a |
For reference, in previous versions of Z3, ascii escape sequence used byte escapes literals in the format |
|
The bug with not setting ascii over programmatic parameter updates is fixed. The format of escape characters has changed. I removed support for the old escape characters to avoid supporting a mixture of escape conventions. The convention of using \u{XYZ} could appear awkward and different from mainstream conventions, but as far as I can tell can be used independently of the character encoding (unless you choose some character range where the printable ascii and escape sequences themselves cannot be expressed. |
When setting the global encoding to
ascii
as seen in the following piece of code:the output is shown in
unicode
:Through a series of tests, it is concluded that the encoding parameter is not set to "ascii". What is the manner to set the encoding to "ascii"?
Note that in earlier versions of z3, the default encoding was ascii.
The text was updated successfully, but these errors were encountered: