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

注意：这绝对是报告时的错误。此后已修复。