For the JFP submission it was a bummer that we needed to write the counterexamples by hand for the register machine. We could add a lot more counterexamples for the final version if we have a good automatic way to shrink and print them (as we do for the stack machine).