Fix string test and change unicode to character in backend

claripy/backends/backend_z3.py

@@ -5,6 +5,7 @@
 import numbers
 import operator
 import os
+import re
 import signal
 import sys
 import threading
@@ -574,6 +575,19 @@ def _abstract_internal(self, ctx, ast, split_on=None):
         z3.Z3_inc_ref(ctx, ast)
         return a
 
+    def replace_unicode(self, match):
+        """
+        Converts a Unicode escape sequence to the corresponding character.
+
+        Args:
+        - match (re.Match): A regex match object containing a Unicode escape sequence.
+
+        Returns:
+        - str: The Unicode character corresponding to the hexadecimal code.
+        """
+        hex_code = match.group(1)
+        return chr(int(hex_code, 16))
+
     def _abstract_to_primitive(self, ctx, ast):
         decl = z3.Z3_get_app_decl(ctx, ast)
         decl_num = z3.Z3_get_decl_kind(ctx, decl)
@@ -629,7 +643,7 @@ def _abstract_to_primitive(self, ctx, ast):
         elif op_name == "INTERNAL":
             seq = z3.SeqRef(ast)
             if seq.is_string():
-                return seq.as_string()
+                return re.sub(r"\\u\{([0-9a-fA-F]+)\}", self.replace_unicode, seq.as_string())
         raise BackendError("Unable to abstract Z3 object to primitive")
 
     def _abstract_bv_val(self, ctx, ast):