问Z3中无文献的三角函数可修复性？

EN

根据官方说法，在Z3中不支持trig。例如，请参见这个问题或这一个。然而，在Z3中有一些无记录的三角函数运算符--例如，它们在回归试验中使用。甚至还有一个内置的符号叫做pi。Z3甚至可以用这些运算符做一些琐碎的证明，例如：

(declare-fun x () Real)
(assert (= (cos pi) x))
(check-sat)
(get-value (x))

回来时：

sat
((x (- 1.0)))

这些操作人员工作不太好。例如，这个小输入文件将导致Z3 4.4.1出现seg错误，或者导致主分支作为此承诺 (Now)的内存使用量急剧增加：

(declare-fun x () Real)
(assert (< (sin x) -1.0))
(check-sat)

我并不感到惊讶的是，一个无文档的特性，而团队认为不存在，不起作用。我的问题是:它们可以修复吗？在Z3中增加什么级别的性能是合理的？我知道我可以用Z3用未解释的函数加上三角恒等式做一些三角证明。Z3团队对此有兴趣吗？