if we are processing the LHS of the |=, the RHS of the |=, the RHS of the rewrite, the requires, and the ensures, why not just process the entire rule? Then you don't need to do all this custom stuff, you just need to wrap the LHS of the |= in the entire rule, and then call the pre-existing code to tweak the side condition.