george.karpenkov added a comment. > The imprecision in the built in solver might result in failure to constrain a > value to zero while the Z3 might be able to do that.
Ah right, that's a good point, we only throw a null-pointer deref/division by zero when the pointer/value is definitely zero. Do you have *motivating* examples though, like an actual code samples where you got a bug and the analyzer does not warn? In my experience, we almost never warn about division by zero anyway, and the null pointer dereference check is too noisy if anything. https://reviews.llvm.org/D49074 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
