clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead;