Please enable the `daikon.PrintInvariants.print_inv_class` configuration option (described in section "
General configuration options", but admittedly hard to find!). Then Daikon will print the Java class that represents each invariant. (The invariant looks to me more like it came from EltOneOf than EltOneOfString, but that is just a guess, without access to the inputs that Daikon ran on.)
You are right that the documentation of EltOneOfString (and some other invariants) is incorrect in that it omits the "elements" that is part of the printed representation. Thank you for pointing that out. I have fixed it in commit a22a297c.
The `Elt` in the class name means that the invariant is about the elements of the array rather than about the array itself.
Suppose that a variable takes on these values:
[1, 2, 3]
[3, 4, 5]
[1, 2, 3]
[1, 2, 3]
[3, 4, 5]
Then an invariant about the array would be that its value is one of { [1, 2, 3], [3, 4, 5] }.
An invariant about the elements would be that the array's elements are one of { 1, 2, 3, 4, 5 }.