LLVM Static Analyzer Integrates Z3 Solver: Eliminating False Positives

LLVM's static analyzer now supports the Z3 constraint solver, significantly improving its ability to filter out false positives. The article demonstrates two methods of using Z3: as an external solver and for refuting false positives. The first method, while completely eliminating false positives, is significantly slower (approximately 15x). The second method, using Z3 for refutation, is faster and more efficient in reducing false positives. Experiments show that enabling Z3 allows the LLVM static analyzer to accurately identify and avoid false positives caused by bitwise operations, resulting in more reliable analysis.