[vintermann]

The divisor is from 0 to 63. The dividend is a variable bit length integer, i.e. a bigint.

[bonzini]

Absolutely not, he needs to compute (63 - x) / 7, where x is computed from a 64-bit integers. There are no bigints involved.

[vintermann]

Well, there are variable length integers involved, since it's as part of a way of representing variable length integers. But it seems you're right that x is just a regular machine int in this context, as an implementation detail. I misunderstood.