See Aurel300/prusti-dev#202 (comment)
Viper blames the enclosing node (e.g. method call statement) for a failed well-definedness check of a native partial operation expression (e.g. a sequence index), which leaves the expression that actually failed in the reason rather than in the offending position.
See Aurel300/prusti-dev#202 (comment)
Viper blames the enclosing node (e.g. method call statement) for a failed well-definedness check of a native partial operation expression (e.g. a sequence index), which leaves the expression that actually failed in the
reasonrather than in theoffendingposition.