z3 - 为什么Z3在网页和本地（分别为unsat/sat）报告不同的查询状态？

Question

正确的结果应该是UNSAT（在线版），但是本地Z3 3.2报告SAT。它还生成了一个有趣的模型，其中包含枚举类型（数据类型）的全域和基数约束。想法？谢谢！

score 2 · Accepted Answer

2

等待结束。4.0 已发布。

于 2012-05-09T02:28:25.867 回答

score 1 · Accepted Answer

这是一个错误。Z3 3.2 不会为您的脚本安装递归数据类型引擎。因此，排序Q和T被视为未解释的排序。Z3 4.0 修复了这个错误。在线版本已经运行 Z3 4.0。这就是您使用在线版本获得正确结果的原因。您可以在 Z3 3.2 中使用以下解决方法。

（设置选项：自动配置假）

2 回答 2