NAME: c_ex01.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex01.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex01.c 

=== Stats ===
   time (s)            : 3.67
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 956
   states saved        : 249
   state matches       : 0
   transitions         : 952
   trace steps         : 248
   valid calls         : 1678
   provers             : z3, cvc4
   prover calls        : 1

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

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex04.c 

=== Stats ===
   time (s)            : 4.05
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1710
   states saved        : 635
   state matches       : 0
   transitions         : 1703
   trace steps         : 634
   valid calls         : 4577
   provers             : z3, cvc4
   prover calls        : 3

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

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex05.c 

=== Stats ===
   time (s)            : 4.4
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3122
   states saved        : 1353
   state matches       : 0
   transitions         : 3110
   trace steps         : 1352
   valid calls         : 13959
   provers             : z3, cvc4
   prover calls        : 2

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

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex06.c 

=== Stats ===
   time (s)            : 4.22
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 2768
   states saved        : 1200
   state matches       : 0
   transitions         : 2761
   trace steps         : 1199
   valid calls         : 12416
   provers             : z3, cvc4
   prover calls        : 2

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

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex07.c 

=== Stats ===
   time (s)            : 5.76
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 5320
   states saved        : 2194
   state matches       : 0
   transitions         : 5288
   trace steps         : 2193
   valid calls         : 37919
   provers             : z3, cvc4
   prover calls        : 1

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

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex08.c 

=== Stats ===
   time (s)            : 4.43
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3172
   states saved        : 1357
   state matches       : 0
   transitions         : 3160
   trace steps         : 1356
   valid calls         : 13991
   provers             : z3, cvc4
   prover calls        : 2

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


Violation 0 encountered at depth 166:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-mpi.cvl:726.6-729.20 "$assert(0, "Process with rank %d reaches an MPI collective routine %s which has an inconsistent datatype specification with at least one of others", \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(432)-1)
  0<=(SIZEOF(435)-1)
  0<=(SIZEOF(445)-1)
  0<=(SIZEOF(476)-1)
  0<=(SIZEOF(479)-1)
  0<=(SIZEOF(483)-1)
  0<=(SIZEOF(486)-1)
  0<=(SIZEOF(490)-1)
  0<=(SIZEOF_INT-1)
  0<=(SIZEOF_REAL-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 c_ex08_inconsist_col.c:25.13-16 "argc"
process 1:
  $mpi_collective_recv at civl-mpi.cvl:339.18-30 "$comm_dequeue" called from
  $mpi_gather at civl-mpi.cvl:451.1-20 "$mpi_collective_recv" called from
  MPI_Gather at mpi.cvl:259.2-12 "$mpi_gather" called from
  _civl_main at c_ex08_inconsist_col.c:45.13-22 "MPI_Gather" called from
  _mpi_process at GeneralTransformer "_civl_argc, (char*[_" inserted by GeneralTransformer.new main function before c_ex08_inconsist_col.c:25.13-16 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before c_ex08_inconsist_col.c:25.13-16 "argc"
process 2:
  $mpi_diff_coroutine_entries at civl-mpi.cvl:726.6-12 "$assert" called from
  MPI_Gather at mpi.cvl:258.2-28 "$mpi_diff_coroutine_entries" called from
  _civl_main at c_ex08_inconsist_col.c:50.13-22 "MPI_Gather" called from
  _mpi_process at GeneralTransformer "_civl_argc, (char*[_" inserted by GeneralTransformer.new main function before c_ex08_inconsist_col.c:25.13-16 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before c_ex08_inconsist_col.c:25.13-16 "argc"
process 3:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before c_ex08_inconsist_col.c:25.13-16 "argc"
process 4:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before c_ex08_inconsist_col.c:25.13-16 "argc"
process 5:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before c_ex08_inconsist_col.c:25.13-16 "argc"
process 6:
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before c_ex08_inconsist_col.c:25.13-16 "argc"

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

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex08_inconsist_col.c 

=== Stats ===
   time (s)            : 3.41
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 391
   states saved        : 166
   state matches       : 0
   transitions         : 389
   trace steps         : 165
   valid calls         : 1480
   provers             : z3, cvc4
   prover calls        : 3

=== Result ===
The program MAY NOT be correct.  See CIVLREP/c_ex08_inconsist_col_log.txt
NAME: c_ex13.c
CITE: \cite{Dummy}
SCALE: {\text{NP=6}}
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex13.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=6 -collectHeaps=false c_ex13.c 

=== Stats ===
   time (s)            : 5.13
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3249
   states saved        : 1422
   state matches       : 0
   transitions         : 3237
   trace steps         : 1421
   valid calls         : 20421
   provers             : z3, cvc4
   prover calls        : 2

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