z3 - 除非使用 PROOF_MODE 选项，否则不饱和响应

Question

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

Answer 1

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

（设置逻辑 QF_AUFLIA）

此逻辑指定脚本将仅包含数组、未解释的函数和整数变量，并且不包含量词。但是，它包含 Real 变量。如果您删除此命令，您将在两种情况下都得到正确答案 (sat)。使用 PROOF_MODE=1 时您得到了不同的答案，因为 Z3 中的某些预处理器不支持证明生成，然后在开启证明生成时它们被禁用。

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