[enhancement] Exhaustive quickchecks

[grebe]

What's hard to do? (limit 100 words)

If the input domain of a quickcheck is small enough, it's natural to want to check exhaustively. It appears that interpreter_main doesn't enforce that each test case is novel, so you can't choose test_count=LARGE_NUMBER st the test is guaranteed to be exhaustive. Even if you could choose LARGE_NUMBER s.t. it would be exhaustive, changing a type of some input could make it too small later, and keeping those up to date seems hard.

Something like quickcheck(exhaustive) would be nice.

Current best alternative workaround (limit 100 words)

Choose a very large test_count. Use a prove quickcheck target so Z3 proves the property.

Your view of the "best case XLS enhancement" (limit 100 words)

Some annotation that you want the property to be checked exhaustively.