Why not use smallcheck?
The premise behind SmallCheck, namely, that
If a program fails to meet its specification in some cases, it almost always fails in some simple case.
is false. There are many practical cases where a minimal counterexample is not that small or simple. Hybrid algorithms provide many examples.
To be concrete, imagine testing a hybrid sorting algorithm, which starts with divide-and-conquer quicksort, but switches to insertion sort once subarrays are less then N elements. On modern hardware typical values of N are [15..20] (say, it’s 18 in vector-algorithms). If you try to test it with SmallCheck you would never ever get into testing quicksort part of it, which could happily remain undefined, because enumerating all arrays up to 18 elements will take too long. But QuickCheck will get there fairly quickly.
Discussion in the ATmosphere