[Z3]Python int too large to convert to C int

Question

from binascii import b2a_hex,a2b_hex
from z3 import *    
def test():
        mystr="005c797800566e69005b"
        mybytes=bytearray(a2b_hex(mystr))
        s=Solver()
        print(mybytes)
        x=[ BitVec("x%s"%i, 32) for i in range(len(mybytes))]
        for i in range(len(mybytes)):
            c = mybytes[i]
            print(i,hex(c))
            print(x[i])
            s.add(((x[i]>>(i%4))^x[i]) == (mybytes[i]))
        if(s.check()==sat):
            model = s.model()
            print(model)
            flag=""
            for i in range(len(mybytes)):
                if(model[x[i]]!=None):
                    print(model[x[i]])
                    flag +=chr(model[x[i]].as_long().real)
        print("flag",flag)

when i use z3 to take a test i get this problem after i ran the code

enter image description here

Answer 1

when i change the version to 4.8.5.0 ,it worked