Z3是否支持带有分层函数符号的扩展EPR逻辑？

一阶逻辑的EPR（有效命题片段）存在一种带函数符号的扩展形式，只要函数的类型结构满足特定要求即可。相关内容已在学术研究中被探讨，也被Voigt的博士论文引用。

Voigt博士论文中给出如下命题：

命题3.14.4（[ARS10, GdM09, Kor13b]）。分层词汇表上的多态∃∀语句的可满足性问题是可判定的。

其中的“分层词汇表”可以包含函数符号，但函数的类型需要遵循对应的结构化规则。

已知Z3针对EPR片段设有专门的处理过程，请问它是否也支持上述这种带分层函数符号的扩展片段？

内容的提问来源于stack exchange，提问作者Nicola Gigante