Here is a smaller repro:

method M(A: set<object>, B: set<object>, C: set<object>, D: set<object>)
  requires C - D <= A - B
  modifies A - B
{
  var cd := C - D;
  if * {
    modify C - D; // does not verify
  } else {
    modify cd; // verifies
  }
}

The problem is that the verifier sometimes tries to be "helpful" in rewriting some proof obligations. In particular, of o in X - Y is a proof obligation, then it rewrites that into o in X && o !in Y. It does this for proof obligations involving modifies A - B and it also does it in translating modify C - D. But it keeps the set-difference operators used in the precondition above and also keep the set-difference operator in the assignment to cd.

By the time things reach the SMT solver, the definition of the subset operator (<=) in the precondition turns into

forall o :: o in SetDifference(C, D) ==> o in SetDifference(A, B)

but that means that conditions like ... in A, ... in B, ... in C, and ... in D do not match the triggers for this quantifier, so it never gets used. In contrast, the proof obligation for modify cd does not go through any rewrite, so the o in cd that proof obligation remains, and since the SMT solver knows cd == SetDifference(C, D), it in effect gets a term o in SetDifference(C, D) and this causes the precondition to trigger.

These "helpful" rewrites seemed innovative in the first year or so of Dafny, which was long before Dafny's auto-triggers were added. Maybe we should get ride of these "helpful" rewrites now, and instead add the following tweak to auto-triggers: if a trigger looks like ..., o in X - Y, ..., then also add the triggers ..., o in X, ... and ..., o in Y, ... (provided those new triggers are legal).

Great that's helpful. I also verified that, replacing

requires C - D <= A - B

by

requires forall a | a in C && a !in D :: a in A && a !in B

everything verifies as expected, which matches your insights. At least, we now have two workarounds.