Does Z3py support "String" and "Sequence"

Question

In Z3, it supports String and Sequence. But does Z3py support them, or do we need to use a string or list from Python? From the latest version, it seemed that the new version supports String and Sequence theories, but I don’t know how to use it. Anyone give me an example about sequence?

Answer 1

Yes, Z3 supports strings and sequences, but the latest public release has only rudimentary support. You will need to compile the last wizard from the source to get all the functions (including the Python API).