Z3(https://github.com/Z3Prover/z3/wiki)是微软开发的一款SMT约束求解器。Ceagle默认使用Z3对待验证属性进行验证求解。