// ignore-test (auxiliary, used by other tests)