> I couldn’t believe that z3 was the best one can do
It probably never is, but if you don't care about a nice solution or don't care about anything past "is it possible?", then z3 and smt2 are amazing. You often don't even need to understand the whole problem. "take constraints, give solution" works great in those situations.
I've tried to use Z3 to find hash collisions in a simple hash, and it was amazingly bad at it. It took forever, whereas just trying random values until some were (multi)colliding was sub-second :-)