rdar://71566576 appears to have been fixed already. Still, add a test case for it to ensure we don’t hit it again.