这是一个生成“sat”的Z3查询 . （我正在运行Z3版本4.8.0，结果在rise4fun Web界面中是相同的 . ）
(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)
然后我得到“不满”，这很好 .
如果我打开校样生成，那么我获得“未知”，这至少是声音 .
(set-option :produce-proofs true)
(assert (forall ((x Real))
(exists ((y Real))
(and (<= 0.0 y) (<= y 1.0) (<= x (* y y))))))
(check-sat)
有人能告诉我发生了什么事吗？我忽视了什么或者它是一个错误吗？
1 回答
注意：这绝对是报告时的错误 . 它已被修复 .