Inferring good loop invariants is a problem that continues to stymie automated software verification tools. One possible solution is to use crowdsourcing to gather input from humans and use that input to guide automated tools. Bounov et al. (2018) were able to use gamification and crowdsourcing to solve verification problems that automated tools could not solve alone. We hypothesize that the design of their game was suboptimal for helping users to find useful invariants, and have designed our own game to test that hypothesis.