Seems to me it would be better still the optimize the whole calculate the rotate is a part of (maybe you don’t really need one of those rotates) but that’s a lot tougher.
It is great to see SMT used for more real problems though!
I would love to see more practical applications of SMT, particularly as intros to newbies.
The (freely available) book "SAT/SMT by Example" [1] shows how a lot of different problems can be tackled with an SMT solver. I highly recommend it!
Check out angr [1], a symbolic execution engine, and claripy [2], its frontend to SMT solvers like z3. Depending on your background, I probably wouldn't describe angr as "for newbies," but claripy is a very clean SMT interface!