civl verify -input_mpi_nprocs_lo=1 -input_mpi_nprocs_hi=10 -DAR_OP=MPI_PROD rm_allreduce_driver.cvl civl_allred_recursive_multiplying.c civl_mpi_funcs.c
CIVL v1.22.r5959 of 2025-03-17 -- https://civl.dev
NP = 1, OPERATOR = 4
Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. NP = 2, OPERATOR = 4
MPI_Irecv is not supported in the MPI blocking implementation.
Violation 0 encountered at depth 280:
CIVL execution violation in p1 [Library: mpi.h, Function: MPI_Irecv] (property: ASSERTION_VIOLATION, certainty: PROVEABLE) at
$assert(0, "MPI_Irecv is not supported in the MPI blocking implementation.")
mpi.cvl:127:2-77 | $assert(0, "MPI_Irecv is not supported in the MPI blocking implementation.")
Assertion: false
-> false
Input:
_civl_argc=X__civl_argc
_civl_argv=X__civl_argv
N=10
x_val=X_x_val
_mpi_nprocs=2
_mpi_nprocs_lo=1
_mpi_nprocs_hi=10
Context:
forall _t : dynamicType . (0 <= CIVL_SIZEOF(_t) - 1)
0<=(SIZEOF_REAL-1)
0<=(X__civl_argc-1)
Call stacks:
process 0:
main@23
process 1:
MPI_Irecv@259 mpi.cvl:127:2 $assert called from
MPIR_Allreduce_intra_recursive_multiplying@360 mpiimpl_cvl.h:12:34 MPI_Irecv called from
_civl_main@459 rm_allreduce_driver.cvl:45:4 MPIR_Allreduce_intra_recursive_multiplying called from
_mpi_process@230 called from
_par_proc0@760
process 2:
$mpi_collective_send@657 civl-mpi-blocking.cvl:322:2 return called from
$mpi_reduce@690 civl-mpi-blocking.cvl:373:4 $mpi_collective_send called from
MPI_Allreduce@274 mpi.cvl:326:2 $mpi_reduce called from
_civl_main@458 rm_allreduce_driver.cvl:43:4 MPI_Allreduce called from
_mpi_process@230 called from
_par_proc0@760
