arrays - Z3 报告一些涉及 (_ as-array ...) 的公式“未知”

Question

Z3（版本 4.4.1）报告我正在编写的工具生成的许多查询“未知”，我已将问题缩小到使用(_ as-array ...)：

(declare-sort MyType)
(declare-fun f (MyType) Bool)
(declare-const a1 (Array MyType Bool))
(declare-const a2 (Array MyType Bool))

; This works fine! (output is SAT)
(push)
(assert (distinct a1 a2))
(check-sat)
(pop)

; This does not! (output is UNKNOWN)
(push)
(assert (distinct a1 (_ as-array f)))
(check-sat)
(pop)

我是否陷入了一个已知无法确定（或在 Z3 中未实现）的案例？