Sanctioned per-model verify override (user-authorized).

Both dzn and nucleos agree the `defersender` leaf has a defer-queue-full
illegal — the VERDICT is identical (`defersender: check: illegal: fail`
/ `error: queue full in model defersender`). Only the counterexample
TRACE shape differs:

  dzn (former golden, line 13):  <queue-full>            (minimal)
  nucleos (verify.override):     p.go / p.return /
                                 <defer> / <queue-full>  (full path to the overflow)

i.e. nucleos prints the fuller system-level path that actually reaches
the overflow, dzn the minimal marker. Counterexample-trace shape is an
impl detail, not a semantic gap (see memory no_overfit_to_dzn), so we
hold nucleos's own output as the expected golden via verify.override
rather than chase dzn's shorter trace. Was previously verify.xfail.

----------------------------------------------------------------------
lts.override.aut — sanctioned per-model LTS override (user-authorized).

dzn cannot produce a finite LTS for this model: `dzn verify --out aut`
emits nothing (the model is illegal/queue-full) and `dzn graph -b lts
-f aut` does not terminate — the external-queue flood (`defer { e.send }`
+ iext `on optional: ack` re-firing) makes the raw state space
unbounded. So there is no dzn .aut to compare against.

nucleos bounds the external queue and produces a finite LTS
(des (0,29,25) — 25 states, 29 transitions), held here as the
nucleos-self golden per no-overfit-to-dzn (same pattern as demon61,
whose dzn mCRL2 backend likewise can't compile). Was lts.xfail
(missing golden).
