[PATCH] D47726: [Analyzer][Z3] Test fixes for Z3 constraint manager

[George Karpenkov via Phabricator via cfe-commits]

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