NAME: any_src-can-deadlock.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 -deadlock=potential any_src-can-deadlock.c 
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 366:
CIVL execution violation in  (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF(<324>) - 1 && 0 <= SIZEOF(<329>) - 1 && 0 <= SIZEOF(<337>) - 1 && 0 <= SIZEOF(<360>) - 1 && 0 <= SIZEOF(<364>) - 1 && 0 <= SIZEOF(<375>) - 1 && 0 <= SIZEOF(<378>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 13, MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
  Enabling predicate: false
ProcessState 1: at location 169, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 169, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false
ProcessState 4: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false
ProcessState 5: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false
ProcessState 6: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false

Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at any_src-can-deadlock.c:43.6-14 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at any_src-can-deadlock.c:52.6-14 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/any_src-can-deadlock_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -deadlock=potential any_src-can-deadlock.c 

=== Stats ===
   time (s)            : 3.47
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 2125
   states saved        : 787
   state matches       : 2
   transitions         : 2120
   trace steps         : 788
   valid calls         : 14552
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/any_src-can-deadlock_log.txt
NAME: any_src-deadlock.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 any_src-deadlock.c 
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 any_src-deadlock.c 

=== Stats ===
   time (s)            : 3.03
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1616
   states saved        : 560
   state matches       : 0
   transitions         : 1612
   trace steps         : 559
   valid calls         : 8835
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
NAME: basic-deadlock.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 basic-deadlock.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 342:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
A deadlock is possible:
  Path condition: 0 <= SIZEOF(<327>) - 1 && 0 <= SIZEOF(<331>) - 1 && 0 <= SIZEOF(<333>) - 1 && 0 <= SIZEOF(<360>) - 1 && 0 <= SIZEOF(<364>) - 1 && 0 <= SIZEOF(<375>) - 1 && 0 <= SIZEOF(<378>) - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false
process p3 (id=3): false
process p4 (id=4): false
process p5 (id=5): false
process p6 (id=6): false

Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_recv at civl-mpi.cvl:199.9-22 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:98.9-18 "$mpi_recv" called from
  _civl_main at basic-deadlock.c:39.6-14 "MPI_Recv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_recv at civl-mpi.cvl:199.9-22 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:98.9-18 "$mpi_recv" called from
  _civl_main at basic-deadlock.c:47.6-14 "MPI_Recv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/basic-deadlock_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 basic-deadlock.c 

=== Stats ===
   time (s)            : 2.76
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 899
   states saved        : 342
   state matches       : 0
   transitions         : 895
   trace steps         : 341
   valid calls         : 2558
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/basic-deadlock_log.txt
NAME: basic-deadlock-comm_dup.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 basic-deadlock-comm_dup.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 598:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
A deadlock is possible:
  Path condition: 0 <= SIZEOF(<386>) - 1 && 0 <= SIZEOF(<391>) - 1 && 0 <= SIZEOF(<393>) - 1 && 0 <= SIZEOF(<418>) - 1 && 0 <= SIZEOF(<422>) - 1 && 0 <= SIZEOF(<433>) - 1 && 0 <= SIZEOF(<436>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false
process p3 (id=3): false
process p4 (id=4): false
process p5 (id=5): false
process p6 (id=6): false

Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_recv at civl-mpi.cvl:199.9-22 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:98.9-18 "$mpi_recv" called from
  _civl_main at basic-deadlock-comm_dup.c:41.6-14 "MPI_Recv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_recv at civl-mpi.cvl:199.9-22 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:98.9-18 "$mpi_recv" called from
  _civl_main at basic-deadlock-comm_dup.c:48.6-14 "MPI_Recv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/basic-deadlock-comm_dup_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 basic-deadlock-comm_dup.c 

=== Stats ===
   time (s)            : 3.62
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1782
   states saved        : 598
   state matches       : 0
   transitions         : 1773
   trace steps         : 597
   valid calls         : 5058
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/basic-deadlock-comm_dup_log.txt
NAME: bcast-deadlock.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 bcast-deadlock.c ##CIVL complains more precisely about the inconsistency
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 77:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-mpi.cvl:683.4-684.81 "$assert($false, "Process with rank %d reaches an MPI collective routine %s which has a different root with at least one of others.", rank ... )":

Assertion: false
        -> false

Input:
  _civl_argc=X__civl_argc
  _civl_argv=X__civl_argv
  _mpi_nprocs=6
  _mpi_nprocs_lo=1
  _mpi_nprocs_hi=X__mpi_nprocs_hi
Context:
  0<=(SIZEOF(321)-1)
  0<=(SIZEOF(323)-1)
  0<=(SIZEOF(325)-1)
  0<=(SIZEOF(351)-1)
  0<=(SIZEOF(355)-1)
  0<=(SIZEOF(366)-1)
  0<=(SIZEOF(369)-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_collective_recv at civl-mpi.cvl:310.18-31 "$comm_dequeue" called from
  $mpi_bcast at civl-mpi.cvl:340.4-24 "$mpi_collective_recv" called from
  MPI_Bcast at mpi.cvl:153.2-12 "$mpi_bcast" called from
  _civl_main at bcast-deadlock.c:29.4-13 "MPI_Bcast" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before bcast-deadlock.c:10.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_diff_coroutine_entries at civl-mpi.cvl:683.4-11 "$assert" called from
  MPI_Bcast at mpi.cvl:152.2-29 "$mpi_diff_coroutine_entries" called from
  _civl_main at bcast-deadlock.c:36.4-13 "MPI_Bcast" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before bcast-deadlock.c:10.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/bcast-deadlock_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 bcast-deadlock.c 

=== Stats ===
   time (s)            : 2.32
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 257
   states saved        : 77
   state matches       : 0
   transitions         : 255
   trace steps         : 76
   valid calls         : 756
   provers             : cvc4, z3, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/bcast-deadlock_log.txt
NAME: collective-misorder.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 collective-misorder.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 400:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-mpi.cvl:678.4-680.32 "$assert($false, "Process with rank %d reaches an MPI collective routine %s while at least one of others are collectively reaching %s.", \n ... )":

Assertion: false
        -> false

Input:
  _civl_argc=X__civl_argc
  _civl_argv=X__civl_argv
  _mpi_nprocs=6
  _mpi_nprocs_lo=1
  _mpi_nprocs_hi=X__mpi_nprocs_hi
Context:
  0<=(SIZEOF(321)-1)
  0<=(SIZEOF(328)-1)
  0<=(SIZEOF(335)-1)
  0<=(SIZEOF(358)-1)
  0<=(SIZEOF(362)-1)
  0<=(SIZEOF(373)-1)
  0<=(SIZEOF(376)-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_collective_recv at civl-mpi.cvl:310.18-31 "$comm_dequeue" called from
  $mpi_bcast at civl-mpi.cvl:340.4-24 "$mpi_collective_recv" called from
  MPI_Bcast at mpi.cvl:153.2-12 "$mpi_bcast" called from
  _civl_main at collective-misorder.c:45.6-15 "MPI_Bcast" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_diff_coroutine_entries at civl-mpi.cvl:678.4-11 "$assert" called from
  MPI_Barrier at mpi.cvl:226.2-29 "$mpi_diff_coroutine_entries" called from
  _civl_main at collective-misorder.c:50.6-17 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/collective-misorder_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 collective-misorder.c 

=== Stats ===
   time (s)            : 2.83
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1026
   states saved        : 400
   state matches       : 0
   transitions         : 1024
   trace steps         : 399
   valid calls         : 2584
   provers             : cvc4, z3, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/collective-misorder_log.txt
NAME: comm-dup-no-free
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 comm-dup-no-error.c ##memory units analysis takes very long
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2438Mb trans=13899 traceSteps=4900 explored=13961 saved=4901 prove=0

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 comm-dup-no-error.c 

=== Stats ===
   time (s)            : 22.0
   memory (bytes)      : 2426404864
   max process count   : 7
   states              : 20523
   states saved        : 6981
   state matches       : 0
   transitions         : 20421
   trace steps         : 6980
   valid calls         : 56698
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
NAME: comm-dup-no-free.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 comm-dup-no-free.c ##report as memory leak
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 516:
CIVL execution violation in p1 (kind: MEMORY_LEAK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "{\nMPI_Comm MPI_COM..." inserted by MPITransformer.function body of _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
An unreachable object (mallocID=1, objectID=1) is detectd in the heap of dyscope d2(id=2).
heap
| objects of malloc 1 at concurrency.cvl:100.2-68 "$barrier barrier=($barrier)$malloc( ... )"
| | 0: struct _barrier[1]
| | | [0]={.place=0, .gbarrier=&<d0>heap.malloc0[0][0]}
| | 1: struct _barrier[1]
| | | [0]={.place=0, .gbarrier=&<d0>heap.malloc0[1][0]}
| objects of malloc 3 at concurrency.cvl:143.2-72 "$collator collator=($collator)$malloc( ... )"
| | 0: struct _collator[1]
| | | [0]={.gcollator=&<d0>heap.malloc2[0][0]}
| | 1: struct _collator[1]
| | | [0]={.gcollator=&<d0>heap.malloc2[1][0]}
| objects of malloc 5 at comm.cvl:131.2-56 "$comm comm=($comm)$malloc( ... )"
| | 0: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc4[0][0]}
| | 1: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc4[1][0]}
| | 2: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc4[2][0]}
| | 3: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc4[3][0]}

Input:
  _civl_argc=X__civl_argc
  _civl_argv=X__civl_argv
  _mpi_nprocs=6
  _mpi_nprocs_lo=1
  _mpi_nprocs_hi=X__mpi_nprocs_hi
Context:
  0<=(SIZEOF(333)-1)
  0<=(SIZEOF(338)-1)
  0<=(SIZEOF(346)-1)
  0<=(SIZEOF(369)-1)
  0<=(SIZEOF(373)-1)
  0<=(SIZEOF(384)-1)
  0<=(SIZEOF(387)-1)
  0<=(SIZEOF_INT-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  _mpi_process at MPITransformer:0.-1-20 "MPI_COMM_WORLD, _m..." inserted by MPITransformer.function call $mpi_comm_destroy before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/comm-dup-no-free_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 comm-dup-no-free.c 

=== Stats ===
   time (s)            : 3.52
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1569
   states saved        : 516
   state matches       : 0
   transitions         : 1563
   trace steps         : 515
   valid calls         : 3691
   provers             : cvc4, z3, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/comm-dup-no-free_log.txt
NAME:  complex-deadlock.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 complex-deadlock.c 
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 367:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
A deadlock is possible:
  Path condition: 0 <= SIZEOF(<329>) - 1 && 0 <= SIZEOF(<334>) - 1 && 0 <= SIZEOF(<336>) - 1 && 0 <= SIZEOF(<361>) - 1 && 0 <= SIZEOF(<365>) - 1 && 0 <= SIZEOF(<376>) - 1 && 0 <= SIZEOF(<379>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false
process p3 (id=3): false
process p4 (id=4): false
process p5 (id=5): false
process p6 (id=6): false

Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_recv at civl-mpi.cvl:199.9-22 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:98.9-18 "$mpi_recv" called from
  _civl_main at complex-deadlock.c:44.6-14 "MPI_Recv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_recv at civl-mpi.cvl:199.9-22 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:98.9-18 "$mpi_recv" called from
  _civl_main at complex-deadlock.c:52.6-14 "MPI_Recv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/complex-deadlock_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 complex-deadlock.c 

=== Stats ===
   time (s)            : 2.79
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 959
   states saved        : 367
   state matches       : 0
   transitions         : 954
   trace steps         : 366
   valid calls         : 2812
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/complex-deadlock_log.txt
NAME: deadlock-config.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 -deadlock=potential deadlock-config.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 156:
CIVL execution violation in  (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF(<295>) - 1 && 0 <= SIZEOF(<300>) - 1 && 0 <= SIZEOF(<328>) - 1 && 0 <= SIZEOF(<332>) - 1 && 0 <= SIZEOF(<343>) - 1 && 0 <= SIZEOF(<346>) - 1 && 0 <= SIZEOF_REAL - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 13, MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
  Enabling predicate: false
ProcessState 1: at location 166, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 166, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 166, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 4: at location 166, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 5: at location 166, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 6: at location 166, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true

Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-12 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-18 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-12 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-18 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-12 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-18 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-12 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-18 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-12 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-18 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-12 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-18 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/deadlock-config_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -deadlock=potential deadlock-config.c 

=== Stats ===
   time (s)            : 2.54
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 596
   states saved        : 156
   state matches       : 0
   transitions         : 594
   trace steps         : 155
   valid calls         : 6582
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/deadlock-config_log.txt
NAME: sendrecv-deadlock.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 -deadlock=potential sendrecv-deadlock.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 346:
CIVL execution violation in  (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>":
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF(<343>) - 1 && 0 <= SIZEOF(<347>) - 1 && 0 <= SIZEOF(<349>) - 1 && 0 <= SIZEOF(<376>) - 1 && 0 <= SIZEOF(<380>) - 1 && 0 <= SIZEOF(<391>) - 1 && 0 <= SIZEOF(<394>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 13, MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
  Enabling predicate: false
ProcessState 1: at location 204, civl-mpi.cvl:240.1-8 "$atomic"
  Enabling predicate: false
ProcessState 2: at location 169, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 169, civl-mpi.cvl:171.4-17 "$comm_enqueue"
  Enabling predicate: true
ProcessState 4: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false
ProcessState 5: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false
ProcessState 6: at location 37, concurrency.cvl:67.2-15 "$barrier_exit"
  Enabling predicate: false

Call stacks:
process 0):
  main at MPITransformer:0.-1-20 "$parfor (int i: 0 ..." inserted by MPITransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 1):
  $mpi_sendrecv at civl-mpi.cvl:240.1-8 "$atomic" called from
  MPI_Sendrecv at mpi.cvl:126.2-15 "$mpi_sendrecv" called from
  _civl_main at sendrecv-deadlock.c:41.3-15 "MPI_Sendrecv" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 2):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at sendrecv-deadlock.c:53.3-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 3):
  $mpi_send at civl-mpi.cvl:171.4-17 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:86.9-18 "$mpi_send" called from
  _civl_main at sendrecv-deadlock.c:61.3-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 4):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at sendrecv-deadlock.c:67.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 5):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at sendrecv-deadlock.c:67.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"
process 6):
  $barrier_call at concurrency.cvl:67.2-15 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:227.2-15 "$barrier_call" called from
  _civl_main at sendrecv-deadlock.c:67.2-13 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_civl_argc, (char*..." inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-14 "argc" called from
  _par_proc0 at MPITransformer:0.-1-0 "i" inserted by MPITransformer.function call _mpi_process before op.h:21.1-10 "Operation" included from civlc.cvh:8.8-14 "<op.h>" included from stdio.cvl:10.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/sendrecv-deadlock_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -deadlock=potential sendrecv-deadlock.c 

=== Stats ===
   time (s)            : 3.08
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 943
   states saved        : 346
   state matches       : 0
   transitions         : 939
   trace steps         : 345
   valid calls         : 6110
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/sendrecv-deadlock_log.txt
NAME: send-recv-ok.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 send-recv-ok.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 send-recv-ok.c 

=== Stats ===
   time (s)            : 2.88
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1616
   states saved        : 560
   state matches       : 0
   transitions         : 1612
   trace steps         : 559
   valid calls         : 3500
   provers             : cvc4, z3, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
NAME: no-error-any_src.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 no-error-any_src.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl
