```py
# EPFL{4ft3r_th15_h0w_h4rD_caN_r3V_8e?}
from z3 import *

num = BitVec("num", 32);
accum = 0

for shift in range(32):
accum = ((num >> shift) & 1) + (accum << 1)

s = Solver()
s.add(num > 0)
# s.add(num < 0x80000000)
s.add(num == accum)

if sat == s.check():
print(s.model())
```