Trace has assignment of NULL to rx_buffers, but assumption changes value. CPAchecker_input_files_61_.zip