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

[Dominic Chen via Phabricator via cfe-commits]

ddcc 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.

I agree, though a number of these are limitations in CSA, and not specifically the backend.

> 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.

I don't plan to set one up either. Just compiling clang/llvm is already very resource intensive.

> 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]

Sounds good.


Repository:
  rC Clang

https://reviews.llvm.org/D47726