z3 - 在 Z3 中跟踪 SAT 约束

Question

我有一些涉及 Bitvectors 的约束，我认为sat即使 Z3 产生了 verdict 也应该如此unsat。我设法将它们简化为一个小例子。

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

标签： z3smt

Answer 1

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