Z3 StringV abstraction broken

[zwimer]

Description

claripy is unable to abstract StringV from z3.

A traceback from: claripy.backend_manager.backends.z3.simplify(claripy.StringV("abc"))

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 92, in z3_condom
    return f(*args, **kwargs)
  File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 1016, in simplify
    o = self._abstract(s)
  File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 92, in z3_condom
    return f(*args, **kwargs)
  File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 414, in _abstract
    return self._abstract_internal(e.ctx.ctx, e.ast)
  File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 536, in _abstract_internal
    a = self._string_constant_from_ast(ctx, ast, decl)
  File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 718, in _string_constant_from_ast
    raise BackendError("Weird Z3 model")
claripy.errors.BackendError: Weird Z3 model

Steps to reproduce the bug

import claripy
a = claripy.StringV("abc")
claripy.backend_manager.backends.z3.simplify(a)

Environment

> mkvirtualenv test
> pip install claripy

Additional context

Before fixing this (and having it work fully), these issues need to be addressed:

• Null characters in z3 strings are abstracted to strings incorrectly Z3Prover/z3#6442