Rating:

A series of linear equations. This solution uses Z3 Prover.

https://advancedpersistentjest.com/2017/11/27/writeups-future-grammarless-tuctf/

Original writeup (https://advancedpersistentjest.com/2017/11/27/writeups-future-grammarless-tuctf/).