This section contains the theory utilised in Schadenfreude: Resurrection. This is ultimately the core of how Schadenfreude: Resurrection works and you should certainly read this, regardless of whether you intend to contribute or simply use Schadenfreude.

I recommend starting with mixed flow graphs, then converting them to SMT statements. More coming shortly