diff --git a/scripts/update_api.py b/scripts/update_api.py index 9e36507d7..7a0f857c3 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -308,7 +308,7 @@ def display_args_to_z3(params): if i > 0: core_py.write(", ") if param_type(p) == STRING: - core_py.write("_to_ascii(a%s)" % i) + core_py.write("_str_to_bytes(a%s)" % i) else: core_py.write("a%s" % i) i = i + 1 @@ -1790,10 +1790,10 @@ if _lib is None: print(" builtins.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext) raise Z3Exception("libz3.%s not found." % _ext) -def _to_ascii(s): +def _str_to_bytes(s): if isinstance(s, str): try: - return s.encode('ascii') + return s.encode('latin-1') except: # kick the bucket down the road. :-J return s @@ -1808,7 +1808,7 @@ else: if s != None: enc = sys.stdout.encoding if enc != None: return s.decode(enc) - else: return s.decode('ascii') + else: return s.decode('latin-1') else: return "" diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 4c143f3ff..4b9b4f1c1 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10038,7 +10038,7 @@ class SeqRef(ExprRef): if self.is_string_value(): string_length = ctypes.c_uint() chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length)) - return string_at(chars, size=string_length.value).decode('ascii') + return string_at(chars, size=string_length.value).decode('latin-1') return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) def __le__(self, other):