我正在尝试调试使用 Z3 API 的程序，我想知道是否有一种方法可以从 API 中或通过给 Z3 一个命令来打印当前的逻辑上下文，希望就好像它已在 SMT-LIB 文件中读取。
This question from 7 years ago 似乎表明有办法做到这一点，但我在 API 文档中找不到它。
我的部分动机是我试图调试我的程序是否因为它创建了一个难以解决的 SMT 问题而运行缓慢，或者减速是否在其他地方。能够以 SMT-LIB 文件的形式查看当前上下文，并在 Z3 中的命令行中运行它，这会更容易。
【问题讨论】：
您所说的“逻辑上下文”不是很清楚。如果你的意思是用户给求解器的所有断言，那么命令：
(get-assertions)
将其作为类似列表的 S 表达式返回；请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 4.2.4 节
但这听起来对您的目的没有用；毕竟它会准确地返回你自己断言的一切。
如果您正在寻找所有学习引理、求解器创建的内部断言等的转储；恐怕 SMTLib 没有办法做到这一点。您甚至可能无法使用编程 API 来做到这一点。 （尽管这需要检查。）这只有通过实际修改 z3 本身的源代码（它是开源的）并放入相关的调试跟踪才能实现。但这需要对 z3 的内部进行大量研究，除非您对 z3 代码库本身非常了解，否则不会有帮助。
我发现运行z3 -v:10 有时可以提供诊断信息；如果您看到它反复打印某些内容，则表明该区域出现了问题。但同样，除非您研究源代码本身，否则它打印的内容和确切含义是猜测工作。
【讨论】：
(get-assertions) 是您的朋友。对应的C-api函数在这里：z3prover.github.io/api/html/…