It seems that the type checker does not catch an assignment to an identifier used in a selection expression on an edge, i.e.
select i : int[0,3];
assign i = 2;
does not give a syntax error. Instead, the verifier throws an exception.
Quantifiers suffer from the same problem. Iterator statements to not cause an exception but a runtime failure during verification.
Fixed on the trunk.