在 Z3 中跟踪 SAT 约束

Question

我有一些涉及位向量的约束，我认为应该是 sat，即使 Z3 产生了判断 unsat。我已经设法将它们简化为一个小例子。

我尝试通过运行z3 -tr:sat test.smt 来跟踪求解器，但没有得到任何跟踪（它只是说unsat）。任何想法为什么这不起作用，或者调试这种情况的替代方法？

Answer 1

您可能想要标记您的约束，然后要求一个未饱和的核心。这将允许您查看发现哪些（希望是一小部分）约束有冲突并从那里进行调试。如果您发布您的示例，我们可以帮助将其设置为 unsat-core 生产。