baloghadamsoftware added a comment.

In, @george.karpenkov wrote:

> The overall point is that writing this kind of code is *extremely* 
> error-prone.

Every modifications on the core is extremely error-prone. That is why we must 
cross check it and only apply it if it is 100% mathematically correct. This 
patch is only WIP for now. Freezing the core in its current state helps us to 
not introduce new errors but also prevents improving the current functionality 
which is not yet sufficient for many of our customers. What I did is not 
hacking, multiplicative operations can be implemented a similar way to additive 
ones, they are just a bit more complex.

> We are actually considering going in a different direction and doing a 
> rollback for the previous rearrangement patches due to some issues.

What issues could it cause since it is guarded by an option? As for the 
rearrangement of the additive operations it was @NoQ's idea but I agree there. 
Actually I feel this rearrangement patch a bit of hacking, but I also agree 
with @NoQ that it may be useful for other checkers as well. That was the reason 
to put it into `SValBuilder` instead of the checker itself. As you may be aware 
of it I originally did the rearrangement inside the checker.

> Could you see whether Z3 visitor would meet your needs?

We will look at it, but please read my previous answer.

cfe-commits mailing list

Reply via email to