NAME: diffusion1d.c
CITE: \cite{siegel-zirkel:2011:fevs-mcs}
SCALE: {\texttt{NPin1,3], NSTEPS, NXin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false diffusion1d.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2448Mb trans=106844 traceSteps=49043 explored=106848 saved=74594 prove=111

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false diffusion1d.c 

=== Stats ===
   time (s)            : 27.17
   memory (bytes)      : 3166175232
   max process count   : 4
   states              : 162071
   states saved        : 110186
   state matches       : 0
   transitions         : 162067
   trace steps         : 71699
   valid calls         : 270891
   provers             : z3, cvc4, cvc3
   prover calls        : 111

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c
CITE: \cite{siegel-zirkel:2011:fevs-mcs}
SCALE: {\texttt{NPX=NPY=2, NSTEPS, NX, NYin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false diffusion2d.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2446Mb trans=41657 traceSteps=17923 explored=41659 saved=26253 prove=45
34s: mem=3020Mb trans=94302 traceSteps=40087 explored=94303 saved=59384 prove=45
49s: mem=2740Mb trans=150572 traceSteps=63794 explored=150574 saved=94856 prove=45
64s: mem=2417Mb trans=207341 traceSteps=87455 explored=207343 saved=130632 prove=45
79s: mem=2137Mb trans=264061 traceSteps=110657 explored=264063 saved=166216 prove=45
94s: mem=1914Mb trans=334496 traceSteps=139703 explored=334498 saved=210544 prove=57
109s: mem=2532Mb trans=386276 traceSteps=161575 explored=386278 saved=243493 prove=57
124s: mem=2820Mb trans=444032 traceSteps=185674 explored=444034 saved=280110 prove=57
139s: mem=3097Mb trans=501651 traceSteps=209600 explored=501653 saved=316699 prove=57
154s: mem=3178Mb trans=578586 traceSteps=241957 explored=578588 saved=366097 prove=65

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false diffusion2d.c 

=== Stats ===
   time (s)            : 160.31
   memory (bytes)      : 3274178560
   max process count   : 5
   states              : 626185
   states saved        : 397023
   state matches       : 0
   transitions         : 626183
   trace steps         : 262366
   valid calls         : 1896521
   provers             : z3, cvc4, cvc3
   prover calls        : 65

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c
CITE: 
SCALE: {\texttt{NPX=NX=3,NPY=NY=1,NSTEPS=2}}
civl verify -enablePrintf=false -collectHeaps=false -inputny=1 -inputnsteps=2 -inputnx=3  -inputNPROCSX=3 -inputNPROCSY=1 diffusion2d.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false -inputny=1 -inputnsteps=2 -inputnx=3 -inputNPROCSX=3 -inputNPROCSY=1 diffusion2d.c 

=== Stats ===
   time (s)            : 4.48
   memory (bytes)      : 919076864
   max process count   : 4
   states              : 2600
   states saved        : 1674
   state matches       : 0
   transitions         : 2598
   trace steps         : 1121
   valid calls         : 6543
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
NAME: wave1d.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin1,4], NSTEPS,NXin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false wave1d.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2459Mb trans=86222 traceSteps=37091 explored=86227 saved=55707 prove=28

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false wave1d.c 

=== Stats ===
   time (s)            : 27.73
   memory (bytes)      : 3155165184
   max process count   : 5
   states              : 131127
   states saved        : 83396
   state matches       : 0
   transitions         : 131122
   trace steps         : 54791
   valid calls         : 261196
   provers             : z3, cvc4, cvc3
   prover calls        : 28

=== Result ===
The standard properties hold for all executions.
NAME: wave1dBad.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin1,4], NSTEPS,NXin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false wave1dBad.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 264:
CIVL execution violation in p1 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at wave1dBad.c:208.5-210.60
	     $assert((oracle[time + 1][first + i + 1] == buf[i]), \
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
	...
    time, first + i, buf[i], oracle[time + 1][first + i + 1]);
                                                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Assertion: (((oracle)[(time+1)])[((first+i)+1)]==*((buf+i)))
        -> -2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0]))==*(&<d5>heap.malloc6[0][1]+0)
        -> (-2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0])))==(-2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0]+((-1/2)*Hp1s5f8o0[0]))*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0])))
        -> (0==((X_u_init[1] + (-1/2)*X_u_init[2] + (-1/2)*X_u_init[0])*(X_c^2) + (X_u_init[1] - 2*X_u_init[0])*(X_c^2) + (-1/2)*X_u_init[1] + X_u_init[0] + (-1/2)*Hp1s5f8o0[0] - 1*((X_u_init[1] + (-1/2)*X_u_init[2] + (-1/2)*X_u_init[0])*(X_c^2) + (X_u_init[1] - 2*X_u_init[0])*(X_c^2) + (-1/2)*X_u_init[1] + X_u_init[0])))||(0==X_c)

Input:
  _civl_argc=X__civl_argc
  _civl_argv=X__civl_argv
  NXB=5
  nx=5
  c=X_c
  NSTEPSB=5
  nsteps=5
  wstep=1
  u_init=X_u_init
  _mpi_nprocs=1
  _mpi_nprocs_lo=1
  _mpi_nprocs_hi=4
Context:
  0<X_c
  0<=(SIZEOF(611)-1)
  0<=(SIZEOF(614)-1)
  0<=(SIZEOF(641)-1)
  0<=(SIZEOF(643)-1)
  0<=(SIZEOF(646)-1)
  0<=(SIZEOF(648)-1)
  0<=(SIZEOF_REAL-1)
  0<=(X__civl_argc-1)
  0!=SIZEOF_REAL
Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before wave1dBad.c:246.13-16 "argc"
process 1:
  printData at wave1dBad.c:208.5-11 "$assert" called from
  write_frame at wave1dBad.c:224.4-12 "printData" called from
  _civl_main at wave1dBad.c:270.6-16 "write_frame" called from
  _mpi_process at GeneralTransformer "_civl_argc, ((char*[" inserted by GeneralTransformer.new main function before wave1dBad.c:246.13-16 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before wave1dBad.c:246.13-16 "argc"

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

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false wave1dBad.c 

=== Stats ===
   time (s)            : 4.53
   memory (bytes)      : 919076864
   max process count   : 2
   states              : 497
   states saved        : 328
   state matches       : 0
   transitions         : 496
   trace steps         : 263
   valid calls         : 1643
   provers             : z3, cvc4, cvc3
   prover calls        : 30

=== Result ===
The program MAY NOT be correct.  See CIVLREP/wave1dBad_log.txt
NAME: gaussJordan_elimination.c
CITE: \cite{siegel-zirkel:2011:fevs-mcs}
SCALE: {\texttt{NPin1,3], ROWin1,COL], COLin1,3]}}
civl verify -enablePrintf=false -collectHeaps=false gaussJordan_elimination.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2446Mb trans=45836 traceSteps=18291 explored=45838 saved=27631 prove=146
34s: mem=3015Mb trans=107443 traceSteps=43067 explored=107445 saved=65044 prove=267
49s: mem=2736Mb trans=168891 traceSteps=67980 explored=168893 saved=102562 prove=395
64s: mem=2515Mb trans=243438 traceSteps=98667 explored=243439 saved=148587 prove=498
79s: mem=2222Mb trans=313394 traceSteps=126984 explored=313395 saved=191367 prove=601

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false gaussJordan_elimination.c 

=== Stats ===
   time (s)            : 85.74
   memory (bytes)      : 2239758336
   max process count   : 4
   states              : 353699
   states saved        : 216454
   state matches       : 0
   transitions         : 353697
   trace steps         : 143682
   valid calls         : 1046381
   provers             : z3, cvc4, cvc3
   prover calls        : 628

=== Result ===
The standard properties hold for all executions.
NAME: matmat_mw.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin2,4], N,L,Min1,3]}}
cd matmat_mw/ && make
civl verify -enablePrintf=false -input_mpi_nprocs_lo=2 -input_mpi_nprocs_hi=4 -inputNB=3 -inputLB=3 -inputMB=3 matmat_mw.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

Error: This feature is not yet implemented: Transform symbolic array (real[X_L*X_M])<lambda i : int . Y16[i div X_M][i%X_M]>[0:=X_b[0][0], 1:=X_b[1 div X_M][1%X_M], 2:=X_b[2 div X_M][2%X_M], 3:=X_b[3 div X_M][3%X_M], 4:=X_b[4 div X_M][4%X_M], 5:=X_b[5 div X_M][5%X_M], 6:=X_b[6 div X_M][6%X_M], 7:=X_b[7 div X_M][7%X_M], 8:=X_b[8 div X_M][8%X_M]] of type real[X_L*X_M]to another type real[X_L][X_M]
NAME: mpi_pi_send.c
CITE: \cite{Dummy}
SCALE: {\texttt{ROUNDS, DARTS, NPin1,2]}}
civl verify -enablePrintf=false -collectHeaps=false mpi_pi_send.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=876Mb trans=27243 traceSteps=10879 explored=27244 saved=17486 prove=383
34s: mem=1416Mb trans=58551 traceSteps=23426 explored=58552 saved=37641 prove=788
49s: mem=1418Mb trans=87876 traceSteps=35115 explored=87877 saved=56432 prove=1194
64s: mem=2435Mb trans=121081 traceSteps=48437 explored=121082 saved=77824 prove=1597

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false mpi_pi_send.c 

=== Stats ===
   time (s)            : 72.71
   memory (bytes)      : 2553806848
   max process count   : 3
   states              : 141929
   states saved        : 91167
   state matches       : 0
   transitions         : 141927
   trace steps         : 56740
   valid calls         : 214922
   provers             : z3, cvc4, cvc3
   prover calls        : 1852

=== Result ===
The standard properties hold for all executions.
NAME: mpi_prime.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin1,4], PRIMESin10,15]}}
civl verify -enablePrintf=false -collectHeaps=false mpi_prime.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=1428Mb trans=26774 traceSteps=9756 explored=26556 saved=14553 prove=381

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false mpi_prime.c 

=== Stats ===
   time (s)            : 27.22
   memory (bytes)      : 1498415104
   max process count   : 5
   states              : 48895
   states saved        : 26708
   state matches       : 298
   transitions         : 49188
   trace steps         : 17701
   valid calls         : 78826
   provers             : z3, cvc4, cvc3
   prover calls        : 576

=== Result ===
The standard properties hold for all executions.
NAME: mpithread_both.c
CITE: \cite{Dummy}
SCALE: {\text{NP=2, THREADSin1,2], VECLEN=5}}
civl verify -enablePrintf=false -collectHeaps=false -inputVECLEN=5 -inputMAXTHRDS=2 -input_mpi_nprocs=2 mpithreads_both.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2454Mb trans=105105 traceSteps=39706 explored=92501 saved=43543 prove=1
34s: mem=2844Mb trans=236573 traceSteps=91043 explored=206005 saved=97765 prove=1

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false -inputVECLEN=5 -inputMAXTHRDS=2 -input_mpi_nprocs=2 mpithreads_both.c 

=== Stats ===
   time (s)            : 37.26
   memory (bytes)      : 2982150144
   max process count   : 7
   states              : 233918
   states saved        : 110868
   state matches       : 32520
   transitions         : 266436
   trace steps         : 101311
   valid calls         : 309910
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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