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.


> 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

Reply via email to