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
> As far as I know the purpose of the cross-check functionality is to execute
> Z3 only on actual bug report paths.
> 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.
cfe-commits mailing list