EDIT: The answer to this question was found later and described here: http://vc3d.tumblr.com/post/73339717794/note-on-triggers

One thing puzzling me currently about making an invariant for this object is why this is admissible:

_(invariant \forall uint i; i < numfaces ==> \mine(&faces[i]) && \mine(faces[i].edge) && \mine(faces[i].edge->next) && \mine(faces[i].edge->next->next) && \mine(faces[i].edge->next->next->next) && faces[i].edge->next->next->next == faces[i].edge )

but separating the parts of that invariant like below is not admissible:

_(invariant \forall uint i; i < numfaces ==> \mine(&faces[i]) && \mine(faces[i].edge) && \mine(faces[i].edge->next) && \mine(faces[i].edge->next->next) && \mine(faces[i].edge->next->next->next) ) _(invariant \forall uint i; i < numfaces ==> faces[i].edge->next->next->next == faces[i].edge )