【发布时间】：2015-12-08 18:53:59
【问题描述】：
在以下命题序列上运行 Z3
(declare-const x Real)
(assert (= 1 (^ x (/ 1 2))))
(check-sat-using qfnra-nlsat)
(get-model)
(eval (= x (^ x (/ 1 2))))
生产
sat
(model
(define-fun x () Real
(- 1.0))
)
Z3(5, 25): ERROR: even root of negative number is not real
请注意，最后一行简单地评估了第 2 行中关于 x 的建议解的方程，因此 Z3 似乎自相矛盾。这是一个错误还是我错过了什么？
【问题讨论】：
-
奇怪的是，将指数中的 1/2 替换为 1/3 会产生正确的解 x=1。
-
奇数根 1, 1/3, 1/5,... 似乎产生了正确的解 x=1，而偶数根 1/2, 1/4, 1/6, ...产生 x=-1。 2/3, 3/4, ... 等不可约分数幂也产生 x=-1
-
对于错误报告，请在我们的问题跟踪器中创建一个新问题：github.com/Z3Prover/z3/issues 谢谢！