Support unicode strings
It seems like the grammar of strings in Why3 is limited to ascii strings, but the corresponding SMT theory specifically supports unicode strings.
We don't even need to support parsing utf-8 strings so long as we allow longer escape sequences for individual characters up to 0x2FFFF
. However, since currently char
is mapped to OCaml's char
type this introduces a conflict.