Z3 FP邏輯：產生意想不到的模型

Question

對於這個問題：http://rise4fun.com/Z3/YNBG

Z3生產模式：

sat 
((s0 FP!val!0)) 

我期待看到真正的數字作爲模型。這幾乎就好像將FP視爲這種情況下未解釋的排序。有沒有辦法讓Z3在這裏產生一個真實的號碼？

Answer 1

感謝您報告此問題。事實上，FPA模型完成中存在一個錯誤。此修補程序已在Codeplex的不穩定分支中提供。

請注意，==（浮點數相等）與NaN總是假的，即在這個例子中，任何s0滿足公式。現在可以正確忽略這些值（在get-model中）或者使用NaN（對於get-value或通常在啓用模型完成時）完成模型。