Running the above code shows that the value of stdout that tracer has is "a\n\n\n". It seems to stop reading stdin correctly after it encounters the first new line.
If the newlines are replaced with a different character, it continues to work as expected.
This issue might be more appropriately put in the angr issues. I'm not sure.
When newlines are encountered in stdin, the scanf simprocedure does not handle them correctly.
Here's an example program
scan_loop.c
With the following input, tracer does not produce the same value for stdout as the actual program.
problem_input.txt
The output of the actual program:
Running the following code does not produce the same output:
Running the above code shows that the value of stdout that tracer has is "a\n\n\n". It seems to stop reading stdin correctly after it encounters the first new line.
If the newlines are replaced with a different character, it continues to work as expected.
working_input.txt
In this case, the output is "a?\nb?\nc?\n", which matches the output of the actual program.
So the problem seems to be with the newline character. Once a newline character is encountered in scanf, further calls to scanf do not work correctly.