Match Term creation (sometimes)

[SpringVaS]

I observed that in one particular PVC, a match term is created that cannot be matched and thus raises an exception upon script interpretation. It happens in the PVC 'List.size/Null' of the ListExample AlgoVerList.dfy when applying the 'expand' rule on the first term in the antecedent this.Valid().
Expected: The term should match. Other PVCs have "simpler" antecedents, where a smaller, more unspecific match term matches this.Valid(). This cannot be guaranteed for all PVCs.

[SpringVaS]

The function parameters for List.Valid(), i.e., this: List and heap(), are replaced by Wildcards "_" when the match term is created. The resultting term cannon be parsed, see Exception stack trace.