ENABLE_JML_RESOLUTION

Sometimes you want the old simple Java name resolution without consideration of any JML annotation. For example, to determine name clashes between Java and JML.