z3 cannot simplify (v << 3) + 1 - (v << 3)

[fkil]

I am working with z3 and making use of simplify. I've encountered an expression that should be easy to simplify, but isn't simplified. Most notably, if one replaces the bitshifts with multiplications, z3 can simplify it. Here's a python snippet to demonstrate it:

import z3

v = z3.BitVec('v', 32)

f1 = (v << 3) + 1 - (v << 3)
f2 = (v * 8) + 1 - (v * 8)

print(z3.simplify(f1))
print(z3.simplify(f2))

I've encountered this behavior on version 4.13.4.

I have the following questions:

• Is there a reason why bitshifts are harder to simplify than multiplications?
• Is there any way to make z3 simplify this? My current approach is to simply replace all bitshifts with multiplication