angr (http://angr.io/) uses Z3 heavily to perform concolic execution, which lets you do things like load up a block of code or an entire program and ask, symbolically, questions like “to get to this point in the binary, what kind if input is necessary?” We use it a lot for CTFs (“the input is of the format ‘flag{[16 ASCII characters]}’, tell me which ones result in the output including the win text”) and security research (“we ran this program symbolically and can prove that this loop accesses only these addresses on all possible executions”).
