Puzzled
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 )
Why don't implications from one invariant affect another? Or should they ordinarily but something is blocking that here?