Symbolic Execution of MPI Programs with One-Sided Communications