While loop and stdin

[Mohammad Akhlaghi]

Dear GNU Bash developers,

We recently confronted the following situation which we do not 
understand. Any insight would be highly appreciated:

The following command works as expected (and prints "1" and "4"):

$ printf "1 2 3\n4 5 6\n" | while read a b c; do echo $a; done
1
4

However, if a command within the while loop reads from standard input, 
the while loop doesn't read that line any more:

$ printf "1 2 3\n4 5 6\n" \
         | while read a b c; do cat /dev/stdin; echo $a; done
4 5 6
1

We were expecting that 'while' reads the full standard input and that 
the 'cat' command would have returned an empty string (for an empty 
standard input). But when 'cat' has read from the standard input, the 
'while' loop has no longer seen the second line that was given to it.

I just wanted to confirm if the result above is the expected way for 
'while' to read from standard input?

The original problem happened for a program in GNU Astronomy Utilities 
(that I am maintaining) which read from standard input by default. If 
the behavior above is expected, I need to modify the behavior of that 
program.

Thank you very much,
Mohammad