//@ ignore-auxiliary