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.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 544:
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(<401>) - 1 && 0 <= SIZEOF(<403>) - 1 && 0 <= SIZEOF(<405>) - 1 && 0 <= SIZEOF(<438>) - 1 && 0 <= SIZEOF(<441>) - 1 && 0 <= SIZEOF(<445>) - 1 && 0 <= SIZEOF(<448>) - 1 && 0 <= SIZEOF(<452>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 14, 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 311, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 311, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 182, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 4: at location 182, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 5: at location 182, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 6: at location 182, 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:224.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:224.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.68
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2761
   states saved        : 1081
   state matches       : 2
   transitions         : 2750
   trace steps         : 1082
   valid calls         : 29111
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.27
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2048
   states saved        : 775
   state matches       : 0
   transitions         : 2042
   trace steps         : 774
   valid calls         : 19212
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 520:
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(<404>) - 1 && 0 <= SIZEOF(<406>) - 1 && 0 <= SIZEOF(<408>) - 1 && 0 <= SIZEOF(<438>) - 1 && 0 <= SIZEOF(<441>) - 1 && 0 <= SIZEOF(<445>) - 1 && 0 <= SIZEOF(<448>) - 1 && 0 <= SIZEOF(<452>) - 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:239.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:239.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)            : 4.18
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1250
   states saved        : 520
   state matches       : 0
   transitions         : 1246
   trace steps         : 519
   valid calls         : 9009
   provers             : z3, cvc4
   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.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 783:
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(<453>) - 1 && 0 <= SIZEOF(<457>) - 1 && 0 <= SIZEOF(<467>) - 1 && 0 <= SIZEOF(<497>) - 1 && 0 <= SIZEOF(<500>) - 1 && 0 <= SIZEOF(<504>) - 1 && 0 <= SIZEOF(<507>) - 1 && 0 <= SIZEOF(<511>) - 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:239.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:239.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)            : 4.97
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2316
   states saved        : 783
   state matches       : 0
   transitions         : 2307
   trace steps         : 782
   valid calls         : 14603
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 113:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-mpi.cvl:712.4-713.80 "$assert(0, "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(388)-1)
  0<=(SIZEOF(393)-1)
  0<=(SIZEOF(395)-1)
  0<=(SIZEOF(427)-1)
  0<=(SIZEOF(430)-1)
  0<=(SIZEOF(434)-1)
  0<=(SIZEOF(437)-1)
  0<=(SIZEOF(441)-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:339.18-30 "$comm_dequeue" called from
  $mpi_bcast at civl-mpi.cvl:369.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:712.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.32
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 302
   states saved        : 113
   state matches       : 0
   transitions         : 300
   trace steps         : 112
   valid calls         : 1029
   provers             : z3, cvc4
   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.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 682:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-mpi.cvl:707.4-709.31 "$assert(0, "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(393)-1)
  0<=(SIZEOF(404)-1)
  0<=(SIZEOF(406)-1)
  0<=(SIZEOF(436)-1)
  0<=(SIZEOF(439)-1)
  0<=(SIZEOF(443)-1)
  0<=(SIZEOF(446)-1)
  0<=(SIZEOF(450)-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:339.18-30 "$comm_dequeue" called from
  $mpi_bcast at civl-mpi.cvl:369.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:707.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.29
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1577
   states saved        : 682
   state matches       : 0
   transitions         : 1575
   trace steps         : 681
   valid calls         : 12471
   provers             : z3, cvc4
   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.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2446Mb trans=14581 traceSteps=4802 explored=14633 saved=4803 prove=1

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

=== Stats ===
   time (s)            : 25.73
   memory (bytes)      : 2565865472
   max process count   : 7
   states              : 25537
   states saved        : 8486
   state matches       : 0
   transitions         : 25435
   trace steps         : 8485
   valid calls         : 168748
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 770:
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 d2(id=2).
heap
| objects of malloc 1 at concurrency.cvl:96.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:148.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:94.2-73 "$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(402)-1)
  0<=(SIZEOF(414)-1)
  0<=(SIZEOF(416)-1)
  0<=(SIZEOF(446)-1)
  0<=(SIZEOF(449)-1)
  0<=(SIZEOF(453)-1)
  0<=(SIZEOF(456)-1)
  0<=(SIZEOF(460)-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.7
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2256
   states saved        : 770
   state matches       : 0
   transitions         : 2250
   trace steps         : 769
   valid calls         : 15044
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 545:
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(<403>) - 1 && 0 <= SIZEOF(<405>) - 1 && 0 <= SIZEOF(<408>) - 1 && 0 <= SIZEOF(<439>) - 1 && 0 <= SIZEOF(<442>) - 1 && 0 <= SIZEOF(<446>) - 1 && 0 <= SIZEOF(<449>) - 1 && 0 <= SIZEOF(<453>) - 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:239.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:239.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.12
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1314
   states saved        : 545
   state matches       : 0
   transitions         : 1308
   trace steps         : 544
   valid calls         : 9413
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 140:
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(<356>) - 1 && 0 <= SIZEOF(<361>) - 1 && 0 <= SIZEOF(<398>) - 1 && 0 <= SIZEOF(<401>) - 1 && 0 <= SIZEOF(<405>) - 1 && 0 <= SIZEOF(<408>) - 1 && 0 <= SIZEOF_REAL - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 14, 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 246, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 246, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 246, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 4: at location 246, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 5: at location 246, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 6: at location 246, civl-mpi.cvl:224.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:224.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:224.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:224.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:224.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:224.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:224.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)            : 3.46
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 575
   states saved        : 140
   state matches       : 0
   transitions         : 567
   trace steps         : 139
   valid calls         : 5830
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 511:
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(<412>) - 1 && 0 <= SIZEOF(<423>) - 1 && 0 <= SIZEOF(<425>) - 1 && 0 <= SIZEOF(<455>) - 1 && 0 <= SIZEOF(<458>) - 1 && 0 <= SIZEOF(<462>) - 1 && 0 <= SIZEOF(<465>) - 1 && 0 <= SIZEOF(<469>) - 1 && 0 <= SIZEOF_INT - 1 && 0 <= X__civl_argc - 1 && 0 <= X__mpi_nprocs_hi - 6
  Enabling predicate: false
ProcessState 0: at location 14, 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 347, civl-mpi.cvl:278.6-18 "$comm_dequeue"
  Enabling predicate: false
ProcessState 2: at location 316, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 3: at location 316, civl-mpi.cvl:224.4-16 "$comm_enqueue"
  Enabling predicate: true
ProcessState 4: at location 182, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 5: at location 182, concurrency.cvl:58.2-6 "$when"
  Enabling predicate: false
ProcessState 6: at location 182, 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:278.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:224.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:224.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              : 1276
   states saved        : 511
   state matches       : 0
   transitions         : 1269
   trace steps         : 510
   valid calls         : 13877
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.26
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2093
   states saved        : 805
   state matches       : 0
   transitions         : 2087
   trace steps         : 804
   valid calls         : 13158
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 5.31
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 6564
   states saved        : 2414
   state matches       : 89
   transitions         : 6570
   trace steps         : 2502
   valid calls         : 53176
   provers             : z3, cvc4
   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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 3.45
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 1241
   states saved        : 351
   state matches       : 0
   transitions         : 1227
   trace steps         : 350
   valid calls         : 2948
   provers             : z3, cvc4
   prover calls        : 1

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