Null characters in z3 strings are abstracted to strings incorrectly

[zwimer]

For example:

null = z3.StringVal("\0").as_string()
print(len(null), null)

Returns 4 \u{}

This does not happen for other characters, validated via:

import z3
for i in range(255):
    if len(z3.StringVal(chr(i)).as_string()) != 1:
        print(i)

This printed out only 0.

I suspect the issue is that some function returns \u{} instead of \u{0}; thus it is not recognized as a unicode character as \u{1} might be.

[zwimer]

If z3 does not permit null bytes within strings, I think this is still invalid behavior.