You can't easily translate generalized unbounded loops into a solver (it introduces quantifiers that make things nasty; e.g. proving something about strcpy(x, n

You can't easily translate generalized unbounded loops into a solver (it introduces quantifiers that make things nasty; e.g. proving something about strcpy(x, n) forall x, n; translates to nested quantifier which gets hairy and requires you to boil oceans, but proving something about strcpy(x, N) for a fixed N is much simpler.) But in this case you can effectively unroll a lot of those loops assuming you can prove the necessary termination criteria about them. Here in your example the criteria is effectively a kind of structural induction on the input bit vector x (because it can be proven forall x. (x > (x & (x-1))), where bitwidth(x) = fixed N) so it's not hard to see it will terminate. So that's what would happen here, and you'd then feed the unrolled bitwise algorithm into Z3 instead.