Yes. It basically turns a reverse engineering task back into regular "forward" engineering, except you are programming with z3's symbolic variables.

Here is an example: https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7...