Tutorial 8 manager - uniqueManager rule fails

[Roy-Certora]

In the Pre-conditions Vs. Valid States section of the tutorial,
the rule uniqueManager fails in calling the function flipOwnership.
Note that the invocation with arbitrary "args" leads to an infeasible state where
the same manager might have two funds from the beginning. I suggest fixing this rule
by calling this function with the given arguments. One can add the else-if statement in the same block:

else if(f.selector == flipOwnership(uint256 , uint256).selector)
{
// I added this if block with the arguments of "f" set as
// the rule arguments - otherwise, this creates a situation where
// there exists another fund (id3) whose owner is one of the previous owners.
flipOwnership(e, fundId1,fundId2);
}
This fixed the rule (but the invariant still fails, as expected).