Z3 小数指数错误（可能）

Question

运行 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 似乎自相矛盾。这是一个错误还是我遗漏了什么？

Answer 1

此示例暴露了处理根对象的工具中的一些错误。已将修复程序签入 master 分支（Z3 现在 returns 此策略未知）。

Z3 fractional exponent bug (maybe)