【发布时间】：2019-04-30 13:42:05
【问题描述】：
我无法弄清楚如何调试 z3。有没有办法查看 SMT 引擎正在“尝试”什么，以便更容易理解为什么它没有看到一个看起来很明显的解决方案以及它在哪里投入了时间？
作为我特定情况下的示例，我正在使用递归函数并设置 z3 以查找函数具有特定结果的输入。 SMT 超时，yadda yadda yadda，结果我递归的东西的基本情况为 0，但如果它变成负数，它会永远递归。 Z3 不知道不要选择负数，所以会卡住。我通过盯着代码发现了这一点，但如果我在某处有一些输出说“尝试 i == -10，尝试 i == -11，等等”，那么问题出在哪里就很明显了。
我仍然遇到不太明显的问题，我怀疑 Z3 仍然卡在循环中。我怎样才能看到它陷入的循环？
【问题讨论】：
-
z3 并没有真正“执行”你的函数，所以严格来说 陷入循环 在 SMT 求解器的上下文中没有任何意义。最有可能发生的事情可能是电子匹配引擎不断产生非生产性实例。话虽如此，您始终可以通过
z3 -v:10等打开详细模式，并让它打印出它在做什么的痕迹。但是，它打印的内容可能不是您期望看到的。虽然仍然有用。 -
这向我显示了
(smt.recfun :increase-depth 19)...(smt.simplifier-done)(smt.searching)之类的东西，但这并没有真正给我任何关于正在实例化的信息。 -
因此我之前的评论是：“然而，它打印的内容可能不是您期望看到的；尽管仍然有用。”