Hamming weight equation in Z3 SMT Sovler

Question

I have a system of equations to solve in which there is some equations of hamming weight. Hamming weight is generally the number of 1's in binary representation of a number. I tried to solve in Z3 SMT Solver, but it outputs an error stating " b'there is no current model". I am trying to find a 32-bit number with a given hamming weight and some equations.

In examples below, I am trying to find a number(0 to 2^5-1) with hamming weight equal to 3.

from z3 import *
s = Solver()
K = [BitVec('k%d'%i,5) for i in range(3)]    

Eq = [K[0]&0x1 + K[0]&0x2 + K[0]&0x4 + K[0]&0x8 + K[0]&0x10 == 3]  #
s.add(Eq)
s.check()
print(s.model())

This gives error "b'there is no current model".

Can anyone help me regarding this problem?

Edit: I put the hamming equation wrong; It will be

Eq = [(K[0]&0x1) +  ((K[0]&0x2)>>1) +  ((K[0]&0x4)>>2) +  ((K[0]&0x8)>>3) +  ((K[0]&0x10)>>4) == 3 ]

Thanks

Answer 1

It's the operator precedence in Python. This works:

Eq = [(K[0]&0x1) + (K[0]&0x2) + (K[0]&0x4) + (K[0]&0x8) + (K[0]&0x10) == 3]

However, you're not actually computing the hamming weight this way. Each of the terms needs to be shifted. E.g. K[0]&0x8 is not zero or one, but 0x8 or 0x0.