Why Can't (V & 65535) >> 15 Be Simplified Further in Z3?

[Invincibl-e]

I am working with Z3 and encountered an issue where an expression involving bitwise operations is not being simplified as expected. Here's the Python code snippet:

from z3 import *

V = BitVec('V', 32)

expr = simplify((V & 65535) << 17 | (V & 65535) >> 15)
print(expr)

In the output, the right-shift operation (V & 65535) >> 15 is not further simplified. I originally expected Z3 to optimize this expression, particularly by eliminating the redundant (V & 65535).

My questions are:

1. Why does Z3 retain the current form of the expression without simplifying the redundancy in (V & 65535)?
2. Are there specific settings, tactics or options that can force Z3 to further optimize this?
3. If this is a known limitation or intentional behavior in Z3, what are the recommended approaches or alternatives for optimizing such expressions?