我正在寻找关于如何将各种编程语言结构转换为 Z3 的讨论，而不限制求解器的效率。
特别是，是否有一种算法和一组最佳实践规则来将一个以延续传递风格表示的函数/程序转换为 Z3？
使用上下文是使用 Z3 来实现编程语言的类型系统，因此解决方案必须高效且增量（例如，在 Z3 实例中保留以前的 Z3 AST）。
我知道 Boogie，但如果可能的话，我正在寻找更轻量级的东西。
在某种程度上限制输入语言的语义是可以接受的，但目前还不能在 SMTLIB 中简单地表达。
我基本上是在寻找关于人们可能会考虑用于各种典型语言结构的不同策略的讨论。
编辑：限制使输入语言不完整并且仅对较小的程序片段（如库中的函数）合理有效，这可能是可以接受的。例如，输入语言可以是一种用于编写“静态检查”库的语言，该库随后被转译为现有动态编程语言的库，并在适当时使用动态运行时断言。