Going beyond QuickCheck: using an SMT solver (based on Rosette) to intelligently generate test inputs that are diverse and hit interesting code paths! https://youtu.be/Br16rvT_C00