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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 395:
CIVL execution violation in  (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before any_src-can-deadlock.c:14.10-13 "argc"
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF(<584>) - 1 && 0 <= SIZEOF(<586>) - 1 && 0 <= SIZEOF(<589>) - 1 && 0 <= SIZEOF(<616>) - 1 && 0 <= SIZEOF(<618>) - 1 && 0 <= SIZEOF(<621>) - 1 && 0 <= SIZEOF(<623>) - 1 && 0 <= SIZEOF(<626>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 16, MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before any_src-can-deadlock.c:14.10-13 "argc"
  Enabling predicate: false
ProcessState 1: at location 329, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 329, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 4: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 5: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 6: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false

Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before any_src-can-deadlock.c:14.10-13 "argc"
process 1:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at any_src-can-deadlock.c:43.6-13 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before any_src-can-deadlock.c:14.10-13 "argc"
process 2:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at any_src-can-deadlock.c:52.6-13 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before any_src-can-deadlock.c:14.10-13 "argc"
process 3:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before any_src-can-deadlock.c:14.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before any_src-can-deadlock.c:14.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before any_src-can-deadlock.c:14.10-13 "argc"
process 6:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at any_src-can-deadlock.c:63.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before any_src-can-deadlock.c:14.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before any_src-can-deadlock.c:14.10-13 "argc"

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)            : 4.76
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2899
   states saved        : 1432
   state matches       : 2
   transitions         : 2899
   trace steps         : 863
   valid calls         : 10382
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.29
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2127
   states saved        : 1002
   state matches       : 0
   transitions         : 2125
   trace steps         : 603
   valid calls         : 7154
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 370:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before basic-deadlock.c:11.10-13 "argc"
A deadlock is possible:
  Path condition: 0 <= SIZEOF(<582>) - 1 && 0 <= SIZEOF(<590>) - 1 && 0 <= SIZEOF(<592>) - 1 && 0 <= SIZEOF(<616>) - 1 && 0 <= SIZEOF(<618>) - 1 && 0 <= SIZEOF(<621>) - 1 && 0 <= SIZEOF(<623>) - 1 && 0 <= SIZEOF(<626>) - 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 "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before basic-deadlock.c:11.10-13 "argc"
process 1:
  $mpi_recv at civl-mpi.cvl:236.9-21 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:97.9-17 "$mpi_recv" called from
  _civl_main at basic-deadlock.c:39.6-13 "MPI_Recv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock.c:11.10-13 "argc"
process 2:
  $mpi_recv at civl-mpi.cvl:236.9-21 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:97.9-17 "$mpi_recv" called from
  _civl_main at basic-deadlock.c:47.6-13 "MPI_Recv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock.c:11.10-13 "argc"
process 3:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock.c:11.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock.c:11.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock.c:11.10-13 "argc"
process 6:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock.c:52.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock.c:11.10-13 "argc"

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)            : 3.91
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1294
   states saved        : 582
   state matches       : 0
   transitions         : 1292
   trace steps         : 369
   valid calls         : 4874
   provers             : z3, cvc4, 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 667:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before basic-deadlock-comm_dup.c:11.10-13 "argc"
A deadlock is possible:
  Path condition: 0 <= SIZEOF(<675>) - 1 && 0 <= SIZEOF(<681>) - 1 && 0 <= SIZEOF(<685>) - 1 && 0 <= SIZEOF(<709>) - 1 && 0 <= SIZEOF(<711>) - 1 && 0 <= SIZEOF(<714>) - 1 && 0 <= SIZEOF(<716>) - 1 && 0 <= SIZEOF(<719>) - 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 "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before basic-deadlock-comm_dup.c:11.10-13 "argc"
process 1:
  $mpi_recv at civl-mpi.cvl:236.9-21 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:97.9-17 "$mpi_recv" called from
  _civl_main at basic-deadlock-comm_dup.c:41.6-13 "MPI_Recv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock-comm_dup.c:11.10-13 "argc"
process 2:
  $mpi_recv at civl-mpi.cvl:236.9-21 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:97.9-17 "$mpi_recv" called from
  _civl_main at basic-deadlock-comm_dup.c:48.6-13 "MPI_Recv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock-comm_dup.c:11.10-13 "argc"
process 3:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock-comm_dup.c:11.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock-comm_dup.c:11.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock-comm_dup.c:11.10-13 "argc"
process 6:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at basic-deadlock-comm_dup.c:56.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before basic-deadlock-comm_dup.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before basic-deadlock-comm_dup.c:11.10-13 "argc"

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)            : 5.01
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2438
   states saved        : 1092
   state matches       : 0
   transitions         : 2436
   trace steps         : 666
   valid calls         : 9469
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 85:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at bcast-deadlock.c:36.4-12
    MPI_Bcast (buf0, buf_size, MPI_INT, 0, MPI_COMM_WORLD);	
    ^^^^^^^^^
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(558)-1)
  0<=(SIZEOF(566)-1)
  0<=(SIZEOF(569)-1)
  0<=(SIZEOF(593)-1)
  0<=(SIZEOF(595)-1)
  0<=(SIZEOF(598)-1)
  0<=(SIZEOF(600)-1)
  0<=(SIZEOF(603)-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before bcast-deadlock.c:10.10-13 "argc"
process 1:
  $mpi_collective_recv at civl-mpi.cvl:331.18-30 "$comm_dequeue" called from
  $mpi_bcast at civl-mpi.cvl:361.4-23 "$mpi_collective_recv" called from
  MPI_Bcast at mpi.cvl:158.2-11 "$mpi_bcast" called from
  _civl_main at bcast-deadlock.c:29.4-12 "MPI_Bcast" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before bcast-deadlock.c:10.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before bcast-deadlock.c:10.10-13 "argc"
process 2:
  $mpi_diff_coroutine_entries at civl-mpi.cvl:708.4-10 "$assert" called from
  MPI_Bcast at mpi.cvl:157.2-28 "$mpi_diff_coroutine_entries" called from
  _civl_main at bcast-deadlock.c:36.4-12 "MPI_Bcast" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before bcast-deadlock.c:10.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before bcast-deadlock.c:10.10-13 "argc"
process 3:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before bcast-deadlock.c:10.10-13 "argc"
process 4:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before bcast-deadlock.c:10.10-13 "argc"
process 5:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before bcast-deadlock.c:10.10-13 "argc"
process 6:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before bcast-deadlock.c:10.10-13 "argc"

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)            : 3.55
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 312
   states saved        : 131
   state matches       : 0
   transitions         : 311
   trace steps         : 84
   valid calls         : 446
   provers             : z3, cvc4, 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 434:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at collective-misorder.c:50.6-16
      MPI_Barrier (comm);
      ^^^^^^^^^^^
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(581)-1)
  0<=(SIZEOF(583)-1)
  0<=(SIZEOF(585)-1)
  0<=(SIZEOF(611)-1)
  0<=(SIZEOF(613)-1)
  0<=(SIZEOF(616)-1)
  0<=(SIZEOF(618)-1)
  0<=(SIZEOF(621)-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before collective-misorder.c:17.10-13 "argc"
process 1:
  $mpi_collective_recv at civl-mpi.cvl:331.18-30 "$comm_dequeue" called from
  $mpi_bcast at civl-mpi.cvl:361.4-23 "$mpi_collective_recv" called from
  MPI_Bcast at mpi.cvl:158.2-11 "$mpi_bcast" called from
  _civl_main at collective-misorder.c:45.6-14 "MPI_Bcast" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before collective-misorder.c:17.10-13 "argc"
process 2:
  $mpi_diff_coroutine_entries at civl-mpi.cvl:703.4-10 "$assert" called from
  MPI_Barrier at mpi.cvl:231.2-28 "$mpi_diff_coroutine_entries" called from
  _civl_main at collective-misorder.c:50.6-16 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before collective-misorder.c:17.10-13 "argc"
process 3:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before collective-misorder.c:17.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before collective-misorder.c:17.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before collective-misorder.c:17.10-13 "argc"
process 6:
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at collective-misorder.c:40.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before collective-misorder.c:17.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before collective-misorder.c:17.10-13 "argc"

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)            : 4.08
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1629
   states saved        : 686
   state matches       : 0
   transitions         : 1628
   trace steps         : 433
   valid calls         : 6035
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/collective-misorder_log.txt
NAME: comm-dup-no-error.c
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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2448Mb trans=17175 traceSteps=4534 explored=17177 saved=7448 prove=1

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

=== Stats ===
   time (s)            : 27.34
   memory (bytes)      : 2567438336
   max process count   : 7
   states              : 27039
   states saved        : 12849
   state matches       : 0
   transitions         : 27037
   trace steps         : 7707
   valid calls         : 104936
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 581:
CIVL execution violation in p1 (kind: MEMORY_LEAK, certainty: PROVEABLE)
at MPITransformer "{\n$scope _civl_root " inserted by MPITransformer.function body of _mpi_process before comm-dup-no-free.c:18.10-13 "argc"
An unreachable object (mallocID=1, objectID=1) is detected in the heap of dyscope d5(id=5).
heap
| objects of malloc 1 at concurrency.cvl:84.2-67 "$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 comm.cvl:136.2-55 "$comm comm=($comm)$malloc( ... )"
| | 0: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc2[0][0]}
| | 1: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc2[1][0]}
| | 2: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc2[2][0]}
| | 3: struct _comm[1]
| | | [0]={.place=0, .gcomm=&<d0>heap.malloc2[3][0]}
| objects of malloc 5 at collate.cvl:110.4-75 "$collator collator = ($collator) ... )"
| | 0: struct _collator[1]
| | | [0]={.place=0, .gcollator=&<d0>heap.malloc4[0][0]}
| | 1: struct _collator[1]
| | | [0]={.place=0, .gcollator=&<d0>heap.malloc4[1][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(589)-1)
  0<=(SIZEOF(592)-1)
  0<=(SIZEOF(594)-1)
  0<=(SIZEOF(621)-1)
  0<=(SIZEOF(623)-1)
  0<=(SIZEOF(626)-1)
  0<=(SIZEOF(628)-1)
  0<=(SIZEOF(631)-1)
  0<=(SIZEOF_INT-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before comm-dup-no-free.c:18.10-13 "argc"
process 1:
  _mpi_process at MPITransformer "MPI_COMM_WORLD, _mpi" inserted by MPITransformer.function call $mpi_comm_destroy before comm-dup-no-free.c:18.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before comm-dup-no-free.c:18.10-13 "argc"
process 2:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before comm-dup-no-free.c:18.10-13 "argc"
process 3:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before comm-dup-no-free.c:18.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before comm-dup-no-free.c:18.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before comm-dup-no-free.c:18.10-13 "argc"
process 6:
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at comm-dup-no-free.c:38.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before comm-dup-no-free.c:18.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before comm-dup-no-free.c:18.10-13 "argc"

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)            : 4.66
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2370
   states saved        : 956
   state matches       : 0
   transitions         : 2369
   trace steps         : 580
   valid calls         : 8682
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 400:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before complex-deadlock.c:11.10-13 "argc"
A deadlock is possible:
  Path condition: 0 <= SIZEOF(<584>) - 1 && 0 <= SIZEOF(<591>) - 1 && 0 <= SIZEOF(<593>) - 1 && 0 <= SIZEOF(<617>) - 1 && 0 <= SIZEOF(<619>) - 1 && 0 <= SIZEOF(<622>) - 1 && 0 <= SIZEOF(<624>) - 1 && 0 <= SIZEOF(<627>) - 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 "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before complex-deadlock.c:11.10-13 "argc"
process 1:
  $mpi_recv at civl-mpi.cvl:236.9-21 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:97.9-17 "$mpi_recv" called from
  _civl_main at complex-deadlock.c:44.6-13 "MPI_Recv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before complex-deadlock.c:11.10-13 "argc"
process 2:
  $mpi_recv at civl-mpi.cvl:236.9-21 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:97.9-17 "$mpi_recv" called from
  _civl_main at complex-deadlock.c:52.6-13 "MPI_Recv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before complex-deadlock.c:11.10-13 "argc"
process 3:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before complex-deadlock.c:11.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before complex-deadlock.c:11.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before complex-deadlock.c:11.10-13 "argc"
process 6:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at complex-deadlock.c:62.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before complex-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before complex-deadlock.c:11.10-13 "argc"

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)            : 4.16
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1368
   states saved        : 630
   state matches       : 0
   transitions         : 1366
   trace steps         : 399
   valid calls         : 5177
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 162:
CIVL execution violation in  (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before deadlock-config.c:8.14-17 "argc"
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF(<533>) - 1 && 0 <= SIZEOF(<535>) - 1 && 0 <= SIZEOF(<559>) - 1 && 0 <= SIZEOF(<561>) - 1 && 0 <= SIZEOF(<564>) - 1 && 0 <= SIZEOF(<566>) - 1 && 0 <= SIZEOF_REAL - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 16, MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before deadlock-config.c:8.14-17 "argc"
  Enabling predicate: false
ProcessState 1: at location 260, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 260, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 260, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 4: at location 260, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 5: at location 260, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 6: at location 260, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true

Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before deadlock-config.c:8.14-17 "argc"
process 1:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-17 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before deadlock-config.c:8.14-17 "argc"
process 2:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-17 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before deadlock-config.c:8.14-17 "argc"
process 3:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-17 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before deadlock-config.c:8.14-17 "argc"
process 4:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-17 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before deadlock-config.c:8.14-17 "argc"
process 5:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-17 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before deadlock-config.c:8.14-17 "argc"
process 6:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at deadlock-config.c:33.4-11 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before deadlock-config.c:8.14-17 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before deadlock-config.c:8.14-17 "argc"

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)            : 11.87
   memory (bytes)      : 1473773568
   max process count   : 7
   states              : 628
   states saved        : 248
   state matches       : 0
   transitions         : 626
   trace steps         : 161
   valid calls         : 1640
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 377:
CIVL execution violation in  (kind: DEADLOCK, certainty: PROVEABLE)
at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before sendrecv-deadlock.c:11.10-13 "argc"
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF(<617>) - 1 && 0 <= SIZEOF(<623>) - 1 && 0 <= SIZEOF(<625>) - 1 && 0 <= SIZEOF(<649>) - 1 && 0 <= SIZEOF(<651>) - 1 && 0 <= SIZEOF(<654>) - 1 && 0 <= SIZEOF(<656>) - 1 && 0 <= SIZEOF(<659>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 16, MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before sendrecv-deadlock.c:11.10-13 "argc"
  Enabling predicate: false
ProcessState 1: at location 382, civl-mpi.cvl:272.6-18 "$comm_dequeue"
  Enabling predicate: false
ProcessState 2: at location 334, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 334, civl-mpi.cvl:221.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 4: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 5: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 6: at location 197, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false

Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before sendrecv-deadlock.c:11.10-13 "argc"
process 1:
  $mpi_sendrecv at civl-mpi.cvl:272.6-18 "$comm_dequeue" called from
  MPI_Sendrecv at mpi.cvl:131.2-14 "$mpi_sendrecv" called from
  _civl_main at sendrecv-deadlock.c:41.3-14 "MPI_Sendrecv" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before sendrecv-deadlock.c:11.10-13 "argc"
process 2:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at sendrecv-deadlock.c:53.3-10 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before sendrecv-deadlock.c:11.10-13 "argc"
process 3:
  $mpi_send at civl-mpi.cvl:221.4-16 "$comm_enqueue" called from
  MPI_Send at mpi.cvl:87.9-17 "$mpi_send" called from
  _civl_main at sendrecv-deadlock.c:61.3-10 "MPI_Send" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before sendrecv-deadlock.c:11.10-13 "argc"
process 4:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at sendrecv-deadlock.c:67.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before sendrecv-deadlock.c:11.10-13 "argc"
process 5:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at sendrecv-deadlock.c:67.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before sendrecv-deadlock.c:11.10-13 "argc"
process 6:
  $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
  $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
  MPI_Barrier at mpi.cvl:232.2-14 "$barrier_call" called from
  _civl_main at sendrecv-deadlock.c:67.2-12 "MPI_Barrier" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before sendrecv-deadlock.c:11.10-13 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before sendrecv-deadlock.c:11.10-13 "argc"

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)            : 4.2
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1329
   states saved        : 591
   state matches       : 0
   transitions         : 1327
   trace steps         : 376
   valid calls         : 5035
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.25
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2174
   states saved        : 1003
   state matches       : 0
   transitions         : 2172
   trace steps         : 604
   valid calls         : 7074
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== 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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 5.03
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 6956
   states saved        : 3952
   state matches       : 89
   transitions         : 7043
   trace steps         : 2385
   valid calls         : 29597
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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

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

=== Stats ===
   time (s)            : 3.65
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1320
   states saved        : 658
   state matches       : 0
   transitions         : 1318
   trace steps         : 386
   valid calls         : 1672
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
