I'm very happy with the Clang static analyzer used with Z3 in the recommended way (for verification, not as the main constraint handler) through CodeChecker [1]. We use it with "cross translation unit" (CTU) support, to analyze call flows across files.<p>As said, there are few false positives. For embedded software the fact that Z3 understand bitfields and bit operations is nice. But in general we found that it makes better use of CTU information than a proprietary tool we're using (and now consider phasing out).<p>When used with cross compiled software the CC+ClangSA combination can be made to work, but is sometimes a bit rough when there are GCC/Clang subtle incompatibilities. But nothing too bad, and CC provided the hooks to work around any issue we found.<p>Even in "verification" mode, Z3 also helps the analysis as I understand from the docs. Some cheap Z3 analysis are used to prune some paths, which also helps the classical range analysis. Those tools must make some approximation to deal with the combinatorial explosion, so pruning useless paths early can help exploring others leading to bugs. So Z3, even in the default mode, is not only to filter out false positive but can also help finding issues.<p>I would highly recommend it for people using C and C++. With those languages the tooling around is very important to (partially) mitigate their known "dangerosity".<p>[1] <a href="https://codechecker.readthedocs.io/en/latest/" rel="nofollow">https://codechecker.readthedocs.io/en/latest/</a>