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!