This post reminds me that I've been wanting to try out ZetZ[0]. It incorporates Z3 into a high-level programming language, and seems to do a lot of what the post talks about automatically.

[0] https://github.com/zetzit/zz