对于这个问题：http ://rise4fun.com/Z3/YNBG
Z3 产生模型：
sat
((s0 FP!val!0))
我期待看到一个真实的数字作为模型。FP对于这种情况，它几乎就像是一种未解释的类型。有没有办法让 Z3 在这里产生一个实数？
问问题
137 次
对于这个问题：http ://rise4fun.com/Z3/YNBG
Z3 产生模型：
sat
((s0 FP!val!0))
我期待看到一个真实的数字作为模型。FP对于这种情况，它几乎就像是一种未解释的类型。有没有办法让 Z3 在这里产生一个实数？
感谢您报告此事。事实上，FPA 的模型完成中存在错误。该修复程序已在Codeplex的不稳定分支中提供。
请注意，==（浮点相等）与 NaN 始终为假，即，在此示例中，anys0满足公式。这些值现在完全正确地省略了（在 get-model 中）或者模型用 NaN 完成（对于 get-value 或通常在启用模型完成时）。