如何让Z3合规识别多态数据类型测试器的良序项？

Z3处理包含多态数据类型的SMT-Lib代码时会触发歧义错误，具体报错：

(error "line 6 column 15: ambiguous function declaration reference, provide full signature to disambiguate (<symbol> (<sort>*) <sort>) X")

触发错误的代码如下：

(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((S 1)) ((par (T) ((X (getX T))))))
(declare-fun x () (S Int))
(define-fun  y () (S (S Int)) (X x))
(assert ((_ is X) y))
(check-sat)
(get-model)

目前有两种临时写法能让Z3正常运行，但都不符合SMT-Lib 2.6规范：

• (assert (is-X y))：cvc5支持该写法，但不属于标准语法范畴
• (assert ((_ is (X ((S Int)) (S (S Int)))) y))：相关评论称其符合标准，但实际不满足SMT-Lib 2.6规范，且cvc5等其他求解器不兼容

现在需要明确两个问题：

1. 有没有严格符合SMT-Lib标准的替代写法？
2. 其他主流求解器（比如MathSAT、Alt-Ergo）对这类多态数据类型判别式的支持情况是怎样的？

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