我有 LLVM 字节码中的描述，我需要作为 Z3 输入传递。如果可以的话，是怎么做到的呢？？如果没有的话有什么工具可以做到吗？
小智 5
可以将 C 代码转换为 Z3 形式的两个工具可以处理：
1）SMACK（https://github.com/smackers/smack）
这使用 LLVM 位码作为中间表示，将带注释的 C 代码转换为 Boogie 语言。然后可以使用Boogie 工具 ( http://boogie.codeplex.com ) 生成可由 Z3 检查的验证条件。然而，手动注释代码可能是一项艰巨的任务。特别是，您必须为 C 函数的所有循环和前置/后置条件编写归纳不变量，足以证明您的程序满足其规范。
2）不明飞行物（https://bitbucket.org/arieg/ufo/wiki/Home）
该工具可以再次通过 LLVM 位码从 C 语言转换为 SMT-LIB Horn 逻辑。结果可以通过 Z3 的定点引擎之一进行检查。在这种方法中，您不必手动注释循环和过程（因为 Z3 自己发现这些注释），但该工具的容量要小得多。