How to compute the upper part of a product of two bit-vectors?
I could use vectors of double the width, do the normal multiplication and then right shift, but that seems rather inefficient. Is there a better way? Perhaps split the vectors into four halves, do four full multiplications of the original width and combine only the upper part?
Alternatively, is there a solver which supports such operation natively?
If you want to know the precise value of the upper part, then zero-extend to double-width, multiply, and grab the upper bits. Since the lower parts will impact every bit on the top part, you can't do any better, asymptotically. If you have a very specific use case that looks at a very specific set of bits in the upper part instead of all; then you might have a more efficient algorithm; but you'd have to derive it yourself for each bit you are interested in. I'm not aware of any solver that supports anything custom for this purpose.
If you don't care about the value of the upper part, but you only care if the multiplication overflows or not, then z3 has custom built-in functions for that. See the paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf
The primitives z3 provides are:
(The paper has details on how you can detect overflow/underflow for other operations we well.)
These operations directly allow you to determine (in an optimal way) if there's overflow/underflow in multiplication. When you don't care about the value of the upper part but merely want to know if an ovrerflow/underflow happened, use these methods. (See the paper cited above for more details. Especially Section 5.3.)