Tags: z3 

Rating: 0

1. Notice that rotating short int values will quickly make the XOR keystream zeros
2. Notice that +- and &^ can be easily tackled by Z3
3. Bruteforce rest of the flag via sha1

Full writeup: https://github.com/p4-team/ctf/tree/master/2019-11-07-defcamp-finals/crypto