String Theory (SMT-like) support

[XVilka]

Just like SMT it would allow better reasoning about strings: https://microsoft.github.io/z3guide/docs/theories/Strings/

The tricky thing is to decide about encoding, Unicode, handling "wide" characters with zeroes inside, handling grapheme clusters, etc.

[ivg]

The Strings Theory sounds like a good addition, though I am not sure about including it in the Core theory. That's kind of the whole idea of Core that it only includes Core computations (and it is already a little bit overextended to my taste, e.g., compare it with the SMT's Core theory, which is much thinner).

So, maybe the issue should be just "Develop the String Theory"?