Z3

微软研究院开发的高性能定理证明器/SMT求解器，广泛用于程序验证和形式化方法中自动求解验证条件