Cannot use inline predicate in unfolding

[ArmborstL]

I use a simple inline predicate inl as an alias for a more complex predicate actual. I would then expect to be able to use inl wherever I can use actual, including in \unfolding. However, that does not work.
Here is a simplified example:

class C {
    int x;
    
    /*@ resource actual(C c) = Perm(c.x, 1);
        inline resource inl(C c) = actual(c); @*/
        
    /*@ requires inl(other);                                   // OK, creates complex "let" expression in Viper
        requires \unfolding actual(other) \in other.x>0;       // OK, simple "unfolding" in Viper
        // requires \unfolding inl(other) \in other.x>0;       // BUG!!! rejected by VerCors as having side effects
    */
    void m(C other) {
        /*@ assert inl(other); */                              // OK, creates complex "let" expression in viper
        /*@ assert \unfolding actual(other) \in other.x>0; */  // OK, simple "unfolding" in Viper
        /*@ assert \unfolding inl(other) \in other.x>0; */     // BUG!!! instead of using "let" expression in Viper, this just turns into "assert other.x>0"
    }
}

In principle, the inline predicate is translated into a let expression in Viper, to wrap the arguments and only evaluate them once.
However, there are two bugs related to this encoding in the context of \unfolding, as indicated in the example above:

1. in the last assert, the entire \unfolding wrapper is just dropped, and only the inner expression other.x>0 is passed to Viper. This will obviously create "Insufficient Permission" errors that make no sense from the perspective of the VerCors user.
2. when used in a contract like requires, VerCors does not even get to the Viper stage, but rejects the program earlier, saying that "This expression may have side effects, but it is in a position where that is not allowed." about the entire \unfolding expression.

I guess that in this case, the let expression needs to be pulled out and wrap the entire unfolding expression in Viper.