Truncate-of-weighted-sum rewrite is too aggressive

[brianhuffman]

Pull request #343 added a rule that simplifies certain bit-selects applied to weighted sums of bitvectors: When the lower n bits are selected, it truncates all coefficients in the weighted sum down to n bits.

It turns out that this is not always desirable, especially when the coefficient is a number like -1. Truncation (for example, from 1024 bits down to 64) can result in a number that is much farther from 0, and that solvers have a hard time dealing with. This problem is showing up in some of the s2n proofs: goals that yices used to handle easily are now transformed into ones that yices takes forever on.

We need to be more conservative with this rewrite: Instead of reducing all coefficients mod 2^n, we should just filter out those terms with coefficients equivalent to 0 mod 2^n.

[robdockins]

That's a really interesting knock-on effect.

Does it makes sense to try to be an intermediate level of aggressive, where we reduce modulo 2^n iff that doesn't increase the distance from 0 in the signed interpretation (i.e. for positive values)? I rather doubt it would help much but shrug.