更改 unsat 查询中断言的顺序后,它变为 sat。
查询结构为:
definitions1
assertions1
definitions2
bad_assertions
check-sat
我使用 Python 的排序函数对 bad_assertions 进行排序,这使得 Unsat 查询成为 Sat。
Z3 版本 4.0、4.1; Ubuntu 12.04
不幸的是,查询非常大,这使得它们难以调试, 所以我可以提供任何其他附加信息。
最佳答案
我设法重现了您问题中报告的问题。这两个例子都是可以满足的。生成 unsat
的脚本暴露了数据类型理论中的一个错误。我修复了该错误,该修复将在 Z3 4.2 中提供。由于这是一个健全性错误,我们将很快发布 4.2 版本。同时,您可以通过在命令行中使用选项 RELEVANCY=0
来解决该错误。
关于z3 - 漏洞?改变断言的顺序会影响可满足性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12281085/