Use QCheck for the random test suite

One of the main motivation for this change is that QCheck allows us to use a shrinker, providing more concise counter examples.