bv2int: simpler translation for plus and times (#5055)

bv2int: simpler translation for plus and times (#5055)

This PR makes the translation of plus and times by:

using plain mod rather than introducing a skolem. If this proves to be a bottleneck, we can try to tackle it where mod is treated in the solver in the future. This will make it easier to introduce support for quantifiers, as we don't need to introduce new variables under quantification.
Making sure everything is binarized in more places of the translation.