No: Z3 proves the Hacker's Delight* trick almost instantly. The implementation above is not actually faster in practice, so it's rarely used; but its equivalence to popcount relies on Z/2^64Z properties that solvers do not seem familiar with.

* This sort of trick is much older than Hacker's Delight, by the way; Knuth tracks it down to the 1950s in Volume 4A.