# Vm
The first script prints out the operations done inside the binary, redirecting the whole equations to a python file along with some necessary changes and solving the equations using Z3 gives the flag
```py
addr= [0x6,0x3,0x0,0x4,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x10,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x11,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x12,0xc,0x1,0x12,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x13,0xd,0x2,0x13,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x14,0xc,0x0,0x14,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x15,0xc,0x0,0x15,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x16,0x3,0x0,0x0,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x17,0xc,0x0,0x17,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x18,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x19,0xc,0x0,0x19,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x1a,0xc,0x0,0x1a,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x1b,0xc,0x0,0x1b,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x1c,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x1d,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x1e,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x1f,0xc,0x1,0x1f,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x20,0xd,0x2,0x20,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x21,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x22,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x23,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x24,0xc,0x0,0x24,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x25,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x26,0xc,0x1,0x26,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x27,0xd,0x2,0x27,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x4,0x0,0x28,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x29,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x2a,0xc,0x0,0x2a,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x2b,0xc,0x1,0x2b,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x2c,0xd,0x2,0x2c,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x2d,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x2e,0xc,0x1,0x2e,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x2f,0xd,0x2,0x2f,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x30,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x31,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x32,0xc,0x0,0x32,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x33,0xc,0x1,0x33,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x34,0xd,0x2,0x34,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x35,0xc,0x0,0x35,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x36,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x37,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x38,0xc,0x0,0x38,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x39,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x3a,0xc,0x0,0x3a,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x3b,0xc,0x1,0x3b,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x3c,0xd,0x2,0x3c,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x3d,0xc,0x0,0x3d,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x3e,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x3f,0xc,0x0,0x3f,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x40,0xc,0x1,0x40,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x41,0xd,0x2,0x41,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x42,0xc,0x0,0x42,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x43,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x44,0xc,0x0,0x44,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x45,0xe,0x3,0x0,0x5,0x0,0x3,0x7,0x42,0x0,0x6,0x0,0x46,0x8,0x0,0x0,0x6,0x0,0x47,0x8,0x0,0x0,0x6,0x0,0x48,0x8,0x0,0x0,0x6,0x0,0x49,0x8,0x0,0x0,0x6,0x0,0x4a,0x8,0x0,0x0,0x6,0x0,0x4b,0x8,0x0,0x0,0x6,0x0,0x4c,0x8,0x0,0x0,0x6,0x0,0x4d,0x8,0x0,0x0,0x6,0x0,0x4e,0x8,0x0,0x0,0x6,0x0,0x0,0x4,0x0,0x0,0x9,0x0,0x0,0x6,0x0,0x4f,0x8,0x0,0x0,0x6,0x0,0x50,0x8,0x0,0x0,0x6,0x0,0x51,0x8,0x0,0x0,0x6,0x0,0x52,0x8,0x0,0x0,0x6,0x0,0x53,0x8,0x0,0x0,0x6,0x0,0x54,0x8,0x0,0x0,0x6,0x0,0x55,0x8,0x0,0x0,0x6,0x0,0x56,0x8,0x0,0x0,0x6,0x0,0x57,0x8,0x0,0x0,0x6,0x0,0x58,0x8,0x0,0x0,0x6,0x0,0x0,0x9,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xba,0x91,0x8b,0x9a,0x8d,0xdf,0x8b,0x97,0x9a,0xdf,0x99,0x93,0x9e,0x98,0xc5,0xdf,0x63,0x8b,0x8a,0x10,0x85,0x8a,0x1,0x8e,0x74,0x8b,0xcc,0x94,0x5f,0x92,0xcb,0xed,0xb0,0x97,0x69,0x91,0x9b,0x5f,0x50,0x40,0x72,0xcf,0x8c,0x1b,0x80,0x9c,0x3c,0x50,0x96,0x6f,0x92,0x40,0x61,0x97,0x8c,0xa0,0x8d,0x90,0x91,0x40,0x61,0xce,0xcf,0xcf,0x90,0x40,0xa1,0x87,0xbc,0x82,0x47,0x6f,0x6f,0x64,0x20,0x4a,0x6f,0x62,0xa,0x54,0x72,0x79,0x20,0x61,0x67,0x61,0x69,0x6e]
values=[0xba,0x91,0x8b,0x9a,0x8d,0xdf,0x8b,0x97,0x9a,0xdf,0x99,0x93,0x9e,0x98,0xc5,0xdf,0x63,0x8b,0x8a,0x10,0x85,0x8a,0x1,0x8e,0x74,0x8b,0xcc,0x94,0x5f,0x92,0xcb,0xed,0xb0,0x97,0x69,0x91,0x9b,0x5f,0x50,0x40,0x72,0xcf,0x8c,0x1b,0x80,0x9c,0x3c,0x50,0x96,0x6f,0x92,0x40,0x61,0x97,0x8c,0xa0,0x8d,0x90,0x91,0x40,0x61,0xce,0xcf,0xcf,0x90,0x40,0xa1,0x87,0xbc,0x82,0x47,0x6f,0x6f,0x64,0x20,0x4a,0x6f,0x62,0xa,0x54,0x72,0x79,0x20,0x61,0x67,0x61,0x69,0x6e]
res=0
num=0
char=[0]*4
flag=[0]*46
ind = 0
print('char=[0]*4')
print('ind=%d'%(0))
while res!=0x65:
v3 = addr[num+1]
v4 = addr[num+2]
v2=0
val = addr[num]
if val == 1:
char[v3]*=v4&0xff
print('char[%d] *= %d&%d'%(v3,v4,0xff))
elif val == 2:
char[v3]-=v4
print('char[%d] -= %d'%(v3,v4))
elif val == 3:
char[v3]= ~(char[v3])&0xff
print('char[%d] = ~char[%d] & %d'%(v3,v3,0xff))
elif val == 4:
char[v3]^=values[v4]&0xff
print('char[%d] ^= values[%d] & %d'%(v3,v4,0xff))
elif val == 5:
char[v3]=char[v4]
print('char[%d] = char[%d] '%(v3,v4))
elif val == 6:
char[v3]=values[v4]
print('char[%d] = values[%d] '%(v3,v4))
elif val == 7:
print('#Done')
break
if char[0]==True:
num+=3
v2=1
print('v2=1')
elif val == 8:
print(chr(char[0]))
elif val == 9:
print('exit')
break
elif val == 10:
char[0]=flag[ind]
ind+=1
print('s.add(char[3]==0)')
print('char[0]=flag[ind]')
print('ind+=1')
elif val == 11:
char[v3] = char[v3] << v4
print('char[%d] = (char[%d] << %d) & %d'%(v3,v3,v4,0xff))
elif val == 12:
char[v3] = char[v3] & values[v4]
print('char[%d] &= values[%d] & %d'%(v3,v4,0xff))
elif val == 13:
char[v3] = char[v3] | values[v4]
print('char[%d] |= values[%d] & %d'%(v3,v4,0xff))
elif val == 14:
char[v3] += char[v4]
print('char[%d] += char[%d] '%(v3,v4))
if v2!=1:
num+=3
res=addr[num]
```
###### script-2
```py
from z3 import *
addr= [0x6,0x3,0x0,0x4,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x10,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x11,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x12,0xc,0x1,0x12,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x13,0xd,0x2,0x13,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x14,0xc,0x0,0x14,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x15,0xc,0x0,0x15,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x16,0x3,0x0,0x0,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x17,0xc,0x0,0x17,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x18,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x19,0xc,0x0,0x19,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x1a,0xc,0x0,0x1a,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x1b,0xc,0x0,0x1b,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x1c,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x1d,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x1e,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x1f,0xc,0x1,0x1f,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x20,0xd,0x2,0x20,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x21,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x22,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x23,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x24,0xc,0x0,0x24,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x25,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x26,0xc,0x1,0x26,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x27,0xd,0x2,0x27,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x4,0x0,0x28,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x29,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x2a,0xc,0x0,0x2a,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x2b,0xc,0x1,0x2b,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x2c,0xd,0x2,0x2c,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x2d,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x2e,0xc,0x1,0x2e,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x2f,0xd,0x2,0x2f,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x30,0xe,0x3,0x0,0xa,0x0,0x0,0x4,0x0,0x31,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x32,0xc,0x0,0x32,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x33,0xc,0x1,0x33,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x34,0xd,0x2,0x34,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x35,0xc,0x0,0x35,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x36,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x37,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x38,0xc,0x0,0x38,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x39,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x3a,0xc,0x0,0x3a,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x3b,0xc,0x1,0x3b,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x3c,0xd,0x2,0x3c,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x3d,0xc,0x0,0x3d,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x3e,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x3f,0xc,0x0,0x3f,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x0,0x40,0xc,0x1,0x40,0xb,0x1,0x1,0x5,0x2,0x1,0xe,0x1,0x0,0xe,0x2,0x0,0xc,0x1,0x41,0xd,0x2,0x41,0xe,0x1,0x2,0x5,0x0,0x1,0x5,0x3,0x1,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x42,0xc,0x0,0x42,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x43,0xe,0x3,0x0,0xa,0x0,0x0,0x5,0x1,0x0,0x4,0x1,0x44,0xc,0x0,0x44,0x1,0x0,0x2,0xe,0x0,0x1,0xe,0x3,0x0,0xa,0x0,0x0,0x3,0x0,0x0,0x4,0x0,0x45,0xe,0x3,0x0,0x5,0x0,0x3,0x7,0x42,0x0,0x6,0x0,0x46,0x8,0x0,0x0,0x6,0x0,0x47,0x8,0x0,0x0,0x6,0x0,0x48,0x8,0x0,0x0,0x6,0x0,0x49,0x8,0x0,0x0,0x6,0x0,0x4a,0x8,0x0,0x0,0x6,0x0,0x4b,0x8,0x0,0x0,0x6,0x0,0x4c,0x8,0x0,0x0,0x6,0x0,0x4d,0x8,0x0,0x0,0x6,0x0,0x4e,0x8,0x0,0x0,0x6,0x0,0x0,0x4,0x0,0x0,0x9,0x0,0x0,0x6,0x0,0x4f,0x8,0x0,0x0,0x6,0x0,0x50,0x8,0x0,0x0,0x6,0x0,0x51,0x8,0x0,0x0,0x6,0x0,0x52,0x8,0x0,0x0,0x6,0x0,0x53,0x8,0x0,0x0,0x6,0x0,0x54,0x8,0x0,0x0,0x6,0x0,0x55,0x8,0x0,0x0,0x6,0x0,0x56,0x8,0x0,0x0,0x6,0x0,0x57,0x8,0x0,0x0,0x6,0x0,0x58,0x8,0x0,0x0,0x6,0x0,0x0,0x9,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xba,0x91,0x8b,0x9a,0x8d,0xdf,0x8b,0x97,0x9a,0xdf,0x99,0x93,0x9e,0x98,0xc5,0xdf,0x63,0x8b,0x8a,0x10,0x85,0x8a,0x1,0x8e,0x74,0x8b,0xcc,0x94,0x5f,0x92,0xcb,0xed,0xb0,0x97,0x69,0x91,0x9b,0x5f,0x50,0x40,0x72,0xcf,0x8c,0x1b,0x80,0x9c,0x3c,0x50,0x96,0x6f,0x92,0x40,0x61,0x97,0x8c,0xa0,0x8d,0x90,0x91,0x40,0x61,0xce,0xcf,0xcf,0x90,0x40,0xa1,0x87,0xbc,0x82,0x47,0x6f,0x6f,0x64,0x20,0x4a,0x6f,0x62,0xa,0x54,0x72,0x79,0x20,0x61,0x67,0x61,0x69,0x6e]
values=[0xba,0x91,0x8b,0x9a,0x8d,0xdf,0x8b,0x97,0x9a,0xdf,0x99,0x93,0x9e,0x98,0xc5,0xdf,0x63,0x8b,0x8a,0x10,0x85,0x8a,0x1,0x8e,0x74,0x8b,0xcc,0x94,0x5f,0x92,0xcb,0xed,0xb0,0x97,0x69,0x91,0x9b,0x5f,0x50,0x40,0x72,0xcf,0x8c,0x1b,0x80,0x9c,0x3c,0x50,0x96,0x6f,0x92,0x40,0x61,0x97,0x8c,0xa0,0x8d,0x90,0x91,0x40,0x61,0xce,0xcf,0xcf,0x90,0x40,0xa1,0x87,0xbc,0x82,0x47,0x6f,0x6f,0x64,0x20,0x4a,0x6f,0x62,0xa,0x54,0x72,0x79,0x20,0x61,0x67,0x61,0x69,0x6e]
char = [0]*4
s=Solver()
flag=[BitVec('a%s'%i,32) for i in range(46)]
ind=0
char[3] = values[0]
char[3] ^= values[0] & 255
char[0]=flag[ind]
ind+=1
char[0] ^= values[16] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[17] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[18] & 255
char[1] &= values[18] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[19] & 255
char[2] |= values[19] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[20] & 255
char[0] &= values[20] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[21] & 255
char[0] &= values[21] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[22] & 255
char[0] = ~char[0] & 255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[23] & 255
char[0] &= values[23] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] ^= values[24] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[25] & 255
char[0] &= values[25] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[26] & 255
char[0] &= values[26] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[27] & 255
char[0] &= values[27] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] ^= values[28] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[29] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[30] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[31] & 255
char[1] &= values[31] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[32] & 255
char[2] |= values[32] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[33] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] ^= values[34] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[35] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[36] & 255
char[0] &= values[36] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] ^= values[37] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[38] & 255
char[1] &= values[38] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[39] & 255
char[2] |= values[39] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] ^= values[40] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[41] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[42] & 255
char[0] &= values[42] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[43] & 255
char[1] &= values[43] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[44] & 255
char[2] |= values[44] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[45] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[46] & 255
char[1] &= values[46] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[47] & 255
char[2] |= values[47] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[48] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] ^= values[49] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[50] & 255
char[0] &= values[50] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[51] & 255
char[1] &= values[51] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[52] & 255
char[2] |= values[52] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[53] & 255
char[0] &= values[53] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[54] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[55] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[56] & 255
char[0] &= values[56] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[57] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[58] & 255
char[0] &= values[58] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[59] & 255
char[1] &= values[59] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[60] & 255
char[2] |= values[60] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[61] & 255
char[0] &= values[61] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[62] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[63] & 255
char[0] &= values[63] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[0] ^= values[64] & 255
char[1] &= values[64] & 255
char[1] = (char[1] << 1) & 255
char[2] = char[1]
char[1] += char[0]
char[2] += char[0]
char[1] &= values[65] & 255
char[2] |= values[65] & 255
char[1] += char[2]
char[0] = char[1]
char[3] = char[1]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[66] & 255
char[0] &= values[66] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[67] & 255
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[1] = char[0]
char[1] ^= values[68] & 255
char[0] &= values[68] & 255
char[0] *= 2&255
char[0] += char[1]
char[3] += char[0]
s.add(char[3]==0)
char[0]=flag[ind]
ind+=1
char[0] = ~char[0] & 255
char[0] ^= values[69] & 255
char[3] += char[0]
char[0] = char[3]
s.add(char[3]==0)
#Done
if s.check()==sat:
b = s.model()
flag=[BitVec('a%s'%i,32) for i in range(46)]
for i in flag:
k = int(str(b[i]))&0xff
print(chr(k),end='')
```
###### flag: `ctf{výrtu4l_m4chine_pr0tection_is_soo_2010_xD}`
###### tags: `vm` `Z3`
Sign in with Wallet
Connect another wallet