```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())```