If Z3 is on here, I just want to mention Triton ( http://triton.quarkslab.com/ http://triton.quarkslab.com/ ) which is a master thesis project from a French (?)

If Z3 is on here, I just want to mention Triton ( http://triton.quarkslab.com/ http://triton.quarkslab.com/ ) which is a master thesis project from a French (?) person and Pin from Intel ( https://software.intel.com/en-us/articles/pin-a-dynamic-binary-instrumentation-tool https://software.intel.com/en-us/articles/pin-a-dynamic-bina... ). With Triton and Pin you can instrument binary software and gather SMT formulas. It basically allows you to know about the binary SMT style. I had to use it in a practical lab to figure out the input of some hashing function (that would almost always hash to 0). By knowing all the constraints, solving it to know what the input should be becomes quite easy (at least easy compared to brute force).