在Ubuntu上编译z3：报错与处理

Posted 2022-01-17 白马负金羁

Z3 is a high performance theorem prover （SMT solver） developed by Microsoft Research. 通过提供API的方式，它支持多种计算机语言，前面的文章中我们演示了在Python中使用z3的方法（通过使用z3py）。

LLVM中的Clang Static Analyzer（CSA）是在Clang编译器基础上构建的软件源代码分析工具，它可以被用来进行bug finding。CSA中默认使用的constraint solver具有一定的局限性，但我们可以选择Z3作为CSA中的SMT solver，这样可以扩展CSA的能力。

通常情况下，Pre-built binaries for stable releases are available，所以在Ubuntu的shell上直接使用下面的命令就可以安装z3了。

sudo apt install z3

但是，如果使用带z3功能的CSA， 就需要在计算机上build z3 from source（并以此为基础编译clang）。本文将介绍在buntu上编译z3的方法（如果你要自己编译z3，就不要使用上面的语句）。

首先需要把z3的源代码下载到本地（地址就是下图中红色圈里的网址） 

git clone https://github.com/Z3Prover/z3.git

也可