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

Question

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

查询结构为:

definitions1
assertions1
definitions2
bad_assertions
check-sat

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

Z3 版本 4.0、4.1； Ubuntu 12.04

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

这里原来是unsat query带有用于混合的标记线和一个简单的 python script在查询中混合行。

Answer 1

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