在unsat查询中更改断言的顺序后，它变为sat。
查询结构为：
definitions1
assertions1
definitions2
bad_assertions
check-sat
我使用Python的sorted函数对bad_assertions进行了排序，这使得Unsat查询成为Sat。
Z3版本4.0、4.1； Ubuntu 12.04
不幸的是，查询量很大，难以调试，
因此，我可以提供其他任何其他信息。
这里最初是unsat query，带有用于混合的标记行，以及一个简单的python script，用于混合查询中的行。
最佳答案
我设法重现了您的问题中报告的问题。这两个例子都是令人满意的。产生unsat的脚本暴露了数据类型理论中的一个错误。我已修复该错误，该修复程序将在Z3 4.2中可用。由于这是一个健全的错误，我们将很快发布4.2版。同时，您可以通过在命令行中使用选项RELEVANCY=0来解决该错误。