Nice write-up. If I find the time it would be interesting to dive a bit deeper than a shallow read and compare with how things are done in Rosette, which I have

Nice write-up. If I find the time it would be interesting to dive a bit deeper than a shallow read and compare with how things are done in Rosette, which I have more experience with than the Z3Py-interface. https://docs.racket-lang.org/rosette-guide/index.html https://docs.racket-lang.org/rosette-guide/index.html