So basically the compressor is aware of opcode structure so uses multiple data streams and contextual encoding for operands. The article doesn't say much about

So basically the compressor is aware of opcode structure so uses multiple data streams and contextual encoding for operands. The article doesn't say much about the use of SMT solver, but my guess is that it transforms opcodes in a way that they run exactly identically as the original (verified by the solver) but compress better. Well-known stuffs in the data compression community, but also hard to execute efficiently.