z3 - 漏洞？更改断言顺序会影响可满足性

Question

在 unsat 查询中更改断言的顺序后，它变为 sat。

查询结构为：

definitions1
assertions1
definitions2
bad_assertions
check-sat

我使用 Python 的 sorted 函数对 bad_assertions 进行排序，这使得 Unsat 查询 Sat。

Z3 版本 4.0、4.1；Ubuntu 12.04

不幸的是，查询非常大，这使得它们难以调试，因此我可以提供任何其他附加信息。

这里最初是带有标记行的未饱和查询，用于混合，以及一个简单的python脚本来混合查询中的行。

Answer 1

我设法重现了您问题中报告的问题。这两个例子都可以满足。生成的脚本unsat暴露了数据类型理论中的一个错误。我修复了这个错误，该修复将在 Z3 4.2 中可用。由于这是一个健全性错误，我们将很快发布 4.2 版。RELEVANCY=0同时，您可以使用命令行中的选项来解决该错误。

Answer 2

根据您的描述，这听起来像是一个错误。sat/unsat 当然不应该依赖于排序。如果打包一个重现文件很困难，那么帮助我们调试问题的一种方法是，一旦您对触发错误的原因有信心，就是使用“open_log()”转储与 Z3 的所有交互的跟踪。您应该在对 Z3 的其他调用之前使用“open_log”。然后，我们可以在没有您的来源的情况下重播日志。