These are some MPI programs. Our goal is to get civl to verify these exactly as they are, translating them automatically to CIVL-C. Right now this doesn't work.