george.karpenkov added a subscriber: mikhail.ramalho. george.karpenkov added a comment.
@ddcc To be completely honest, I see a few design issues with the current implementation of Z3 backend, the main one being that it checks satisfiability after every single exploded node. To the best of my knowledge, reasonable scalability would not be achieved with such an approach, and I'm not sure how feasible would it be to change it without rewriting most of the checkers. Thus we currently do not plan to set up a Z3 bot, but if you wish to maintain we certainly can provide pointers on how this can be done. > The test approach is what @dcoughlin suggested in > https://reviews.llvm.org/D28952, where the tests are run using each > constraint manager that is available Apologies for conflicting instruction. Now that @mikhail.ramalho is working on refutation with Z3 it might not make sense to force the user to run all tests with Z3 at all times. What do you think if we introduce `ninja check-clang-analyzer` to run the analyzer tests, and `ninja check-clang-analyzer-z3` to run all the analyzer tests with Z3? [there might be another ninja target for running all analyzer tests, I just don't remember which one. But at the end of the day there should be away to run analyzer tests without Z3 even when Z3 is linked in] Repository: rC Clang https://reviews.llvm.org/D47726 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits