idk what the hell that other guy did, but i did it in z3

Original writeup (https://blog.mmaekr.com/2020/06/25/redpwnctf2020-smart-solver/).