Conditional pointer invariant
At exit of
LinkedList.insert(Object x, LinkedListItr p)
if (p ¹ null and p.current ¹ null) then
size(header.closure(next)) =
    size(orig(header.closure(next))) + 1
else
header.closure(next)) =
  orig(header.closure(next))
This is an actual invariant that Daikon detected.
There are other invariants at that program point, but I don’t show them here.

“This is a complex but practical invariant.”
Explain it:  walk people through it.

Now I will demonstrate how Daikon detects invariants like the ones I just showed you.