george.karpenkov added a comment. @baloghadamsoftware @xazax.hun we've had very promising results with using Z3 for refutation so far, almost at no cost, see Mikhail's recent email on cfe-dev (and sometimes at a negative cost!). Do you still not want to try it first? False negatives could be addressed as well separately (e.g. by giving a checkers an option to cross-check the report with a more expensive solver before throwing), currently false positives are a far more pressing problem.
https://reviews.llvm.org/D49074 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
