Fix div, mod, pointer-diff in bitvector mode

1. `is_representable` is used at the result type, losing the information necessary for the check it's supposed to do.
2. Make sure the SMT division/remainder/modulus operations we use for Core `rem_f` and `rem_t` are the right ones.