This is wild: compiling SMT problems to C++ then using coverage guided fuzzing to find solutions! https://github.com/delcypher/jfs