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 :-)