Does Z3 support EPR logic with stratified function symbols?

[nicola-gigante]

There is an extension of the EPR fragment of first-order logic with functions symbols, as long as the sorts of the functions are structured in the right way. This is studied in this paper here (cited as [ARS10] below), and also cited in the PhD thesis by Voigt here. In the latter this is stated as follows:

Proposition 3.14.4 ([ARS10, GdM09, Kor13b]). The satisfiability problem for multi-sorted ∃*∀* sentences over a stratified vocabulary is decidable.

where a "stratified vocabulary" can contain function symbols but, indeed, with sorts structured accordingly.

If I'm not wrong, Z3 has ad-hoc procedures for the EPR fragment. Does it, by chance, support this extended fragment as well?