Using Ctrl and Shift together in a keystroke sometimes fails due to the fact
that the Ctrl+Shift modifier combination appears to cause the subsequent
keypresses to be ignored. Modifier combinations that do not contain both Ctrl
and Shift appear to work normally.
A BIOS update fixed it.