solve (751B)
1#!/usr/bin/env python3 2 3from z3 import * 4 5nums = [int(l) for l in open("msg.txt").read().split("\n")[1:] if l != ""] 6 7s = Solver() 8 9flag = [BitVec(f"flag{i}", 8) for i in range(len(nums))] 10a = BitVec("A", 56) 11b = BitVec("B", 56) 12seed = BitVec("SEED", 56) 13 14state = seed 15state = state * a + b 16for i,num in enumerate(nums): 17 state = state * a + b 18 s.add(Extract(7, 0, state) ^ flag[i] == num) 19 s.add(flag[i] & 0x80 == 0) 20 21s.add(flag[0] == ord(b"C")) 22s.add(flag[1] == ord(b"S")) 23s.add(flag[2] == ord(b"C")) 24s.add(flag[3] == ord(b"G")) 25s.add(flag[4] == ord(b"{")) 26s.add(flag[-1] == ord(b"}")) 27 28while str(s.check()) == "sat": 29 m = s.model() 30 for fc in flag: 31 print(chr(int(str(m[fc]))), end="") 32 s.add(fc != m[fc]) 33 print() 34