Symbolic Verification of MPI Programs with Non-deterministic Synchronizations