为什么 Z3 不能证明/承认 'is_int' 在某些操作下是封闭的？

Question

例如，以下查询超时：

(declare-const x Real)
(declare-const y Real)
(assert (is_int x))
(assert (is_int y))
(assert (not (is_int (+ x y))))
(check-sat)

据我所知，Z3 的Real是数学实数，而不是具有微妙语义的机器实数。承认某些操作保留is_int有什么问题吗？

Answer 1

Z3 将其简化为解决混合整数线性问题，这是较弱的领域之一。在这种情况下，它最终会产生无休止的分支和切割。