[isabelle] Nitpick Codatatype - No Counterexample found

Dear all,
I am trying to use nitpick to find counterexample over (potentially) infinite lists. While playing with nitpick I encountered a strange behavior:
    Nitpick seems to be unable to find counterexamples, if a message occurs twice in the list
An Example:
codatatype 'a::type llist = LNil | LCons 'a "'a llist"
(* Notice that "a" occurs twice *)
lemma "LCons (a::nat) (LCons a LNil) ≠ z"
  nitpick[expect=none]  (* Should find something! *)
(* Allowing different messages, now nitpick can find something *)
lemma "LCons (a::nat) (LCons b LNil) ≠ z"
  nitpick[expect=genuine]   (* is working *)
With the normal (finite) list datatype, this problem does not occur.
Does anybody know the cause & how to fix it?
Sebastian Stüber
Sebastian Stüber, M.Sc.RWTH           |    Software Engineering
Lehrstuhl für Software Engineering    |  RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany   |  https://www.se-rwth.de
Phone ++49 241 80-21352          

Attachment: nitpick_test.thy
Description: nitpick_test.thy

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.