Added a correctness property, which seems to have a longish counterexample, found by fairz3. Is there a simpler counterexample?