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

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

=== Stats ===
   time (s)            : 4.2
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 988
   states saved        : 464
   state matches       : 0
   transitions         : 986
   trace steps         : 264
   valid calls         : 1047
   provers             : z3, cvc4, cvc3
   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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.32
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 1826
   states saved        : 891
   state matches       : 0
   transitions         : 1824
   trace steps         : 566
   valid calls         : 1880
   provers             : z3, cvc4, cvc3
   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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.24
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3262
   states saved        : 1742
   state matches       : 0
   transitions         : 3260
   trace steps         : 1164
   valid calls         : 6195
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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

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

=== Stats ===
   time (s)            : 4.09
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3035
   states saved        : 1610
   state matches       : 0
   transitions         : 3033
   trace steps         : 1056
   valid calls         : 5853
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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

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

=== Stats ===
   time (s)            : 5.54
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 5816
   states saved        : 3479
   state matches       : 0
   transitions         : 5814
   trace steps         : 2275
   valid calls         : 25623
   provers             : z3, cvc4, cvc3
   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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.31
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3349
   states saved        : 1788
   state matches       : 0
   transitions         : 3347
   trace steps         : 1208
   valid calls         : 6334
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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


Violation 0 encountered at depth 138:
CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at c_ex08_inconsist_col.c:50.13-22
	  mpi_err = MPI_Gather((void*)myray,1,MPI_INT, 
	            ^^^^^^^^^^
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(641)-1)
  0<=(SIZEOF(645)-1)
  0<=(SIZEOF(649)-1)
  0<=(SIZEOF(673)-1)
  0<=(SIZEOF(675)-1)
  0<=(SIZEOF(678)-1)
  0<=(SIZEOF(680)-1)
  0<=(SIZEOF(683)-1)
  0<=(SIZEOF_INT-1)
  0<=(SIZEOF_REAL-1)
  0<=(X__civl_argc-1)
  0<=(X__mpi_nprocs_hi-6)
  0!=SIZEOF_REAL
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:331.18-30 "$comm_dequeue" called from
  $mpi_gather at civl-mpi.cvl:447.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:722.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.64
   memory (bytes)      : 649592832
   max process count   : 7
   states              : 401
   states saved        : 199
   state matches       : 0
   transitions         : 400
   trace steps         : 137
   valid calls         : 648
   provers             : z3, cvc4, cvc3
   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.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.85
   memory (bytes)      : 919076864
   max process count   : 7
   states              : 3302
   states saved        : 1781
   state matches       : 0
   transitions         : 3300
   trace steps         : 1211
   valid calls         : 11520
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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