问除非使用PROOF_MODE选项，否则Unsat响应
EN

Stack Overflow用户

提问于 2011-08-10 22:00:31

回答 1查看 209关注 0票数 2

我使用Z3来证明为实时任务系统获得的调度的健壮性。当我检查这个脚本http://www.cs.ru.nl/~georgeta/script.smt2时，我得到了一个unsat响应。但是，当我使用PROOF_MODE=1选项时，响应是sat。在前一种情况下，可能会出什么问题？

发布于 2011-08-10 23:54:08

我下载了你的例子。指定的逻辑不正确，命令：

(设置逻辑QF_AUFLIA)

此逻辑指定脚本将仅包含数组、未解释的函数和整数变量，而不包含任何限定符。但是，它包含实数变量。如果删除此命令，则在两种情况下都将获得正确答案(sat)。在使用PROOF_MODE=1时，您得到了不同的答案，因为Z3中的一些预处理器不支持校样生成，当启用校样生成时，它们将被禁用。

话虽如此，我们修复了Z3 2.19中的许多错误。新的3.0版本将很快发布。您已经可以使用我们提交给SMT-COMP的预发布版本。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/7012033

复制

相似问题

问除非使用PROOF_MODE选项，否则Unsat响应EN