I think I have found out where the problem is. In fact, the encoding of the interactive input is determined by sys.stdin.encoding, but only in the case that it is a file object (see
https://hg.python.org/cpython/file/d356e68de236/Parser/tokenizer.c#l890 and the implementation of tok_stdin_decode). For example, by default on my system sys.stdin has encoding cp852.