If you're willing to overlook that Z3 is a more general SMT solver, it's a useful tool for one-off problems where raw brute-force is inefficient.

I used this to proof-of-concept an attack on Seahash[1]; this was the first time I'd ever used an SMT solver, but it was really very straightforward.

[1] https://gitlab.redox-os.org/redox-os/tfs/issues/5#note_9768