[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added subscribers: dcoughlin, george.karpenkov, NoQ.
mikhail.ramalho added a comment.

Hi,

> Just a bit of context and to have some expectation management regarding
>  this patch. The main purpose of this implementation was to back a thesis.
>  It was made under a very serious time pressure and the main goal was to be
>  able to measure on real world projects as soon as possible and in the
>  meantime to be flexible so we can measure multiple configurations (like
>  incremental solving).
> 
> So the goal was a flexible proof of concept that is sensible to measure in
>  the shortest possible time. After the thesis was done, Reka started to work
>  an another GSoC project, so she had no time to review the code with the
>  requirements of upstreaming in mind. Nevertheless we found that sharing the
>  proof of concept could be useful for the community.  So it is perfectly
>  reasonable if you disagree with some design decisions behind this patch,
>  because the requirements for the thesis (in the short time frame) was very
>  different from the requirements of upstreaming this work. In a different
>  context these decisions made perfect sense.

Just want to comment here and give thanks again for the first version of
the refutation code. It's being really helpful to develop the approach this
code as a base; things would definitely be slower if I had to start it from
scratch.

Thanks!


https://reviews.llvm.org/D45517