baloghadamsoftware added a comment.

In, @george.karpenkov wrote:

> @baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about 
> instead using Z3 cross-check functionality recently added, to solve this and 
> all other similar problems instead?

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.

As we discussed with @dcoughlin at the Euro LLVM 2018 the community should 
consider a new constraint manager, which is in between the range-based one and 
the Z3 both feature and performance wise. However, this is something long term, 
until then we should improve the existing one  as far as reasonable. I am sure 
that multiplicative operations can be solved similarly to the additive ones.

cfe-commits mailing list

Reply via email to