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.