Dafny should issue a warning when an annotation is not supported

[mschlaipfer]

In https://stackoverflow.com/questions/58310238/assertion-violation-in-mvs-with-dafny-but-it-is-verified-in-rise4fun a user tries to use {:arith 2} in assert {:arith 2} forall b,e,x,t,p :: (0 <= t <= e && p * power(x,t) == power(b,e) && t > 0 ) ==> (0 <= t-1 <= e && p * x * power(x,t-1) == power(b,e)); instead of the flag -arith:2. {:arith 2} has no effect. Dafny should probably issue a warning in such cases.

[davidcok]

The implementation issue here is that checks for attributes simply ask whether a given attribute relevant at some program point is in the list of attributes for the entity in question. And those checks are very distributed. There is no central list (in the implementation) of the strings used as attributes.