refactor(bv): Simplify bv2nat mapping using right shifts

The bv2nat mapping is able to record an integer expression for each
bit-vector extraction, but we only need to record arithmetic right
shifts since we encode an extraction `bv<i, j>` as `(bv asr j) - (bv asr
i) * 2^(j - i + 1)`.

This ensures we can't accidentally leave bogus extractions in the map.

Author: bclement-ocp