#include <mpi.h>

$input int _mpi_nprocs_hi= 2;
//$assume(_mpi_nprocs==1);

int main(void) {

}
