Since the default is now to ignore the counterexamples when checking test output, we bring back counterexample checks in tests where the counterexample is (mostly) deterministic.