Conflict between strategies with the same shortcut
When several strategies have the same shortcut (including the empty string), attempting to use one of them always calls the topmost one in why3.conf. Omitting the shortcut line in the conf file is equivalent to setting shortcut="", so this forces users to set unique shortcuts for all strategies even if they do not want to use these shortcuts.