Using Z3 to model the Instructions
Author: [0xec](https://twitter.com/0xec_)
```# Author: 0xec# https://0xec.blogspot.com/# https://twitter.com/0xec_from z3 import *
def dword_from_bytes(b):    return Concat(b[3], b[2], b[1], b[0])
def swap_endian(b):    b3 = Extract(31, 24, b)    b2 = Extract(23, 16, b)    b1 = Extract(15, 8, b)    b0 = Extract(7, 0, b)    return Concat(b0, b1, b2, b3)
def main():    flag = [BitVec('c' + str(i), 8)  for i in range(16)]    shuffle = [2, 6, 7, 1, 5 , 0xb, 9, 0xe, 3, 0xf, 4, 8, 0xa, 0xc, 0xd, 0]
    # pshufb  xmm0, xmmword [rel SHUFFLE]    output = list(map(lambda x: flag[x], shuffle))
    p3 = dword_from_bytes(output[0:4])    p2 = dword_from_bytes(output[4:8])    p1 = dword_from_bytes(output[8:12])    p0 = dword_from_bytes(output[12:16])
    # paddd   xmm0, xmmword [rel ADD32]    p3 = (p3 + 0xdeadbeef)    p2 = (p2 + 0xfee1dead)    p1 = (p1 + 0x13371337)    p0 = (p0 + 0x67637466)
    output = Concat(swap_endian(p3),                     swap_endian(p2),                     swap_endian(p1),                     swap_endian(p0))
    xor_bytes = [0x76, 0x58, 0xb4, 0x49, 0x8d, 0x1a, 0x5f, 0x38, 0xd4, 0x23, 0xf8, 0x34, 0xeb, 0x86, 0xf9, 0xaa]
    # pxor    xmm0, xmmword [rel XOR]    xor_val = int.from_bytes(bytearray(xor_bytes), byteorder="big")    output = output ^ xor_val
    s = Solver()
    for i in range(16):        high = ((16 - i) * 8) - 1        low = ((16 - i) * 8) - 8        s.add(flag[i] == Extract(high, low, output))
    s.add(flag[0] == ord('C'))    s.add(flag[1] == ord('T'))    s.add(flag[2] == ord('F'))    s.add(flag[3] == ord('{'))
    if s.check() == sat:        m = s.model()        print(bytes(map(lambda x: m[x].as_long(), flag)).decode())
if __name__ == '__main__':    main()```
### Output
```$ python3.7 solve.pyCTF{S1MDf0rM3!}```