I was following the Z3 sequences tutorial here: https://microsoft.github.io/z3guide/docs/theories/Sequences/ Would anyone know if there is a similar tutorial on modeling sequences in the Z3 Python API, instead of the SMTLIB format at that link? Thank you in advance!