[tokenrove]

One of my favorite uses is concolic testing which has really been enabled by SMT solvers (of which Z3 is one of the best): http://en.wikipedia.org/wiki/Concolic_testing

Check out MS's Code Digger, which uses Z3 as well: http://research.microsoft.com/en-us/projects/codedigger/

[TheLoneWolfling]

I wonder if that could be implemented as an extension to AFL.

I.e. mutate random values for a while, then use an SMT solver to try to find any remaining code paths that haven't been followed by AFL.

I have a feeling AFL would be faster for "simple" paths, but an SMT solver may be handy for getting those last few paths.

[ulber]

My experience with concolic testing has been that single path satisfiability queries tend to be quite cheap and it's actually a bit challenging to write the tooling around the solver in such a way that the solver would actually become the bottleneck. This is not to say that combinations of concolic testing with other testing methods is not an interesting research topic :)

[rurban]

Then rather use cmbc, which does exactly that. It translates C code into SMT rules, allows assertions on symbolic variables and solves them. And note that for harder crypto problems Z3 is not the best, it's just the easiest to use.