[PATCH] D49074: [Analyzer] [WIP] Basic support for multiplication and division in the constraint manager

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added a comment.

> What issues could it cause since it is guarded by an option?

I've meant the rearrangement. Actually, I would like to apologize for that point, I thought it was causing some issues, but it wasn't, we've just checked it yesterday.

> As far as I know the purpose of the cross-check functionality is to execute Z3 only on actual bug report paths.

Yes.

> This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.


https://reviews.llvm.org/D49074