Z3：非线性算术和量词——错误的结果？

Question

这是一个 Z3 查询，其结果是“sat”。 （我正在运行 Z3 版本 4.8.0，rise4fun 网络中的结果相同 界面。）

(assert (forall ((x Real))
        (exists ((y Real))
                (and (<= 0.0 y) (<= y 1.0) (<= x (* y y))))))
(check-sat)

但是，这个公式应该是不可满足的！不是每个实数 小于或等于 0 到 1 之间数字的平方。

如果我对连词中的公式重新排序，结果会发生变化：

(assert (forall ((x Real))
        (exists ((y Real))
                (and (<= x (* y y)) (<= 0.0 y) (<= y 1.0)))))
(check-sat)

然后我得到“unsat”，这很好。

如果我打开证明生成，那么我会得到“未知”，它位于 声音最小。

(set-option :produce-proofs true)

(assert (forall ((x Real))
        (exists ((y Real))
                (and (<= 0.0 y) (<= y 1.0) (<= x (* y y))))))
(check-sat)

有人可以告诉我发生了什么吗？我是否忽略了什么 还是一个错误？

Answer 1

注意：在报告时这绝对是一个错误。它已经被修复了。