除非使用 PROOF_MODE 选项，否则响应不饱和
我使用 Z3 来证明实时任务系统获得的调度的稳健性。当我检查此脚本 http://www.cs.ru.nl/~georgeta/ script.smt2 我得到了一个不满意的回复。但是，当我使用 PROOF_MODE=1 选项时，响应是 sat。在前一种情况下可能会出现什么问题？
I am using Z3 for proving the robustness of schedules obtained for real time task systems. When I check this script http://www.cs.ru.nl/~georgeta/script.smt2 I get an unsat response. However, when I use the PROOF_MODE=1 option, the response is sat. What could possibly go wrong in the former case?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
我下载了你的例子。指定的逻辑不正确，命令：
此逻辑指定脚本将仅包含数组、未解释的函数和整数变量，并且不包含量词。但是，它包含实数变量。
如果删除此命令，在这两种情况下您都会得到正确的答案 (sat)。
当使用 PROOF_MODE=1 时，您得到了不同的答案，因为 Z3 中的某些预处理器不支持证明生成，然后当打开证明生成时它们将被禁用。
话虽如此，我们在 Z3 2.19 中修复了许多错误。新版本3.0即将发布。
您已经可以使用我们提交到 SMT-COMP 的预发行版本。
I downloaded your example. The specified logic is incorrect, command:
This logic specifies that the script will contain only arrays, uninterpreted functions and integer variables, and no quantifiers. However, it contains Real variables.
If you remove this command, you will get the correct answer (sat) in both cases.
You got a different answer when using PROOF_MODE=1 because some preprocessors in Z3 do not support proof generation, then they are disabled when proof generation is turned on.
That being said, we fixed many bugs in Z3 2.19. The new version 3.0 will be released soon.
You can already use the pre-release version we submitted to SMT-COMP.