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

2018-06-04 Thread Mikhail Ramalho via cfe-commits
> > > Awesome! Does it mean that the optimization for adding less constraints > was in fact buggy? > > I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. > > 2. Could it be something unrelated to your

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

2018-06-01 Thread Mikhail Ramalho via cfe-commits
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 i