NAME: diffusion1d.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$NX,NSTEPS$\leq$5,1$\leq$NP$\leq$3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (91.5 files/s, 19125.3 lines/s)"
1,C,21,24,164
civl verify -enablePrintf=false  diffusion1d.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
18s: mem=1325Mb trans=60636 traceSteps=39628 explored=61021 saved=40852 prove=145

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

=== Stats ===
   time (s)            : 29.93
   memory (bytes)      : 1120403456
   max process count   : 4
   states              : 118272
   states saved        : 79279
   state matches       : 90
   transitions         : 117440
   trace steps         : 76553
   valid calls         : 463080
   provers             : z3, cvc4, cvc3
   prover calls        : 146

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$NX,NY,NSTEPS$\leq$5,NPX=NPY=2}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (84.6 files/s, 30874.7 lines/s)"
1,C,26,65,274
civl verify -enablePrintf=false  diffusion2d.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
18s: mem=1274Mb trans=10798 traceSteps=7106 explored=10882 saved=7388 prove=49
33s: mem=1041Mb trans=34897 traceSteps=22700 explored=35182 saved=23634 prove=49
48s: mem=856Mb trans=58474 traceSteps=38056 explored=58957 saved=39645 prove=49
63s: mem=620Mb trans=83649 traceSteps=54541 explored=84353 saved=56835 prove=49
78s: mem=718Mb trans=114820 traceSteps=75214 explored=115751 saved=78347 prove=49
93s: mem=738Mb trans=139150 traceSteps=91070 explored=140285 saved=94901 prove=49
108s: mem=841Mb trans=163845 traceSteps=107181 explored=165193 saved=111703 prove=49
123s: mem=1014Mb trans=191410 traceSteps=125278 explored=193013 saved=130580 prove=49
139s: mem=1056Mb trans=221033 traceSteps=144962 explored=222853 saved=151072 prove=49
154s: mem=1291Mb trans=248320 traceSteps=162835 explored=250376 saved=169761 prove=49
169s: mem=1494Mb trans=278271 traceSteps=182464 explored=280603 saved=190247 prove=49
184s: mem=1497Mb trans=317737 traceSteps=208853 explored=320375 saved=217791 prove=49
199s: mem=1482Mb trans=346296 traceSteps=227571 explored=349200 saved=237339 prove=49
214s: mem=1492Mb trans=378624 traceSteps=248880 explored=381829 saved=259608 prove=49
229s: mem=1495Mb trans=421280 traceSteps=277374 explored=424817 saved=289382 prove=49
244s: mem=1770Mb trans=467760 traceSteps=308156 explored=471635 saved=321563 prove=49

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

=== Stats ===
   time (s)            : 247.07
   memory (bytes)      : 1859125248
   max process count   : 5
   states              : 489379
   states saved        : 333897
   state matches       : 0
   transitions         : 485418
   trace steps         : 319977
   valid calls         : 2473368
   provers             : z3, cvc4, cvc3
   prover calls        : 49

=== Result ===
The standard properties hold for all executions.
NAME: mpi{\U}prime.c
CITE: \cite{LLNL:MPI:URL}
TYPE: $\text{M}$
SCALE: {\texttt{\{PRIMES\}$\subseteq$[10, 15],1$\leq$NP$\leq$4}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (95.7 files/s, 13304.0 lines/s)"
1,C,9,25,105
civl verify -enablePrintf=false  mpi_prime.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 13.61
   memory (bytes)      : 1384644608
   max process count   : 5
   states              : 28281
   states saved        : 14864
   state matches       : 0
   transitions         : 28276
   trace steps         : 14201
   valid calls         : 79342
   provers             : z3, cvc4, cvc3
   prover calls        : 382

=== Result ===
The standard properties hold for all executions.
NAME: mpi{\U}pi{\U}send.c
CITE: \cite{LLNL:MPI:URL}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$DARTS,ROUNDS,NP$\leq$2}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (92.3 files/s, 15591.9 lines/s)"
1,C,11,38,120
civl verify -enablePrintf=false  mpi_pi_send.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
18s: mem=1328Mb trans=13476 traceSteps=6946 explored=13542 saved=7192 prove=581
33s: mem=1192Mb trans=29021 traceSteps=14997 explored=29166 saved=15517 prove=1166
48s: mem=1076Mb trans=46361 traceSteps=23989 explored=46592 saved=24813 prove=1805
63s: mem=988Mb trans=64617 traceSteps=33479 explored=64940 saved=34637 prove=2501
78s: mem=866Mb trans=82752 traceSteps=42898 explored=83166 saved=44374 prove=3161
93s: mem=756Mb trans=99342 traceSteps=51512 explored=99839 saved=53285 prove=3831

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

=== Stats ===
   time (s)            : 101.43
   memory (bytes)      : 731906048
   max process count   : 3
   states              : 112922
   states saved        : 60328
   state matches       : 0
   transitions         : 112357
   trace steps         : 58321
   valid calls         : 305872
   provers             : z3, cvc4, cvc3
   prover calls        : 4241

=== Result ===
The standard properties hold for all executions.
NAME: sum{\U}array.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$NX$\leq$20,1$\leq$NP$\leq$5}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (95.2 files/s, 8571.3 lines/s)"
1,C,6,12,72
civl verify -enablePrintf=false  sum_array.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false sum_array.c 

=== Stats ===
   time (s)            : 13.22
   memory (bytes)      : 1393033216
   max process count   : 6
   states              : 81852
   states saved        : 54838
   state matches       : 580
   transitions         : 81366
   trace steps         : 52777
   valid calls         : 439555
   provers             : z3, cvc4, cvc3
   prover calls        : 89

=== Result ===
The standard properties hold for all executions.
NAME: wave1d.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$NX,NSTEPS$\leq$5,1$\leq$NP $\leq$3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (86.5 files/s, 22743.0 lines/s)"
1,C,36,33,194
civl verify -enablePrintf=false  wave1d.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
18s: mem=1318Mb trans=43063 traceSteps=26819 explored=43398 saved=28097 prove=99
33s: mem=1090Mb trans=68599 traceSteps=43158 explored=69189 saved=45355 prove=176
48s: mem=946Mb trans=79844 traceSteps=50374 explored=80555 saved=52994 prove=229

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

=== Stats ===
   time (s)            : 53.55
   memory (bytes)      : 896532480
   max process count   : 5
   states              : 98091
   states saved        : 64813
   state matches       : 90
   transitions         : 97216
   trace steps         : 61572
   valid calls         : 420943
   provers             : z3, cvc4, cvc3
   prover calls        : 240

=== Result ===
The standard properties hold for all executions.
NAME: wave1dBad.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$NX,NSTEPS$\leq$5,1$\leq$NP$\leq$3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (88.5 files/s, 23900.2 lines/s)"
1,C,39,39,192
civl verify -enablePrintf=false  wave1dBad.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
Error: disagreement at time 2 position 0: saw -4*(X5[1]*(X3^4))+X5[2]*X3^4+5*(X5[0]*(X3^4))+3*(X5[1]*(X3^2))+-6*(X5[0]*(X3^2))+Hop1s2f2o0[0]*X3^2+X5[0], expected -4*(X5[1]*(X3^4))+X5[2]*X3^4+5*(X5[0]*(X3^4))+3*(X5[1]*(X3^2))+-6*(X5[0]*(X3^2))+X5[0]

Violation 0 encountered at depth 280:
CIVL execution violation in p1(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at wave1dBad.c:197.5-192 "$assert((oracle[time +  ... )":

Input variables:
_gen_argc=X0
_gen_argv=(CHAR[10][])X1
NXB=5
nx=5
c=X3
NSTEPSB=5
nsteps=5
wstep=1
u_init=(real[5])X5
_mpi_nprocs=1
_mpi_nprocs_lo=1
_mpi_nprocs_hi=4

Context: 0<X3 && 0<=SIZEOF_REAL+-1 && 0<=-1*X0+9 && 0<=X0+-1

Assertion: $assert((((oracle)[(time+1)])[((first+i)+1)]==*((buf+i))), &((_anon_11)[0]), time, (first+i), *((buf+i)), ((oracle)[(time+1)])[((first+i)+1)])
-> -4*(X5[1]*(X3^4))+X5[2]*X3^4+5*(X5[0]*(X3^4))+3*(X5[1]*(X3^2))+-6*(X5[0]*(X3^2))+X5[0]==*(&<d9>heap.malloc0[0][1]+0)
-> -4*(X5[1]*(X3^4))+X5[2]*X3^4+5*(X5[0]*(X3^4))+3*(X5[1]*(X3^2))+-6*(X5[0]*(X3^2))+X5[0]==-4*(X5[1]*(X3^4))+X5[2]*X3^4+5*(X5[0]*(X3^4))+3*(X5[1]*(X3^2))+-6*(X5[0]*(X3^2))+Hop1s2f2o0[0]*X3^2+X5[0]
-> 0==Hop1s2f2o0[0]*X3^2

Call stacks:

process p0 (id=0):
  _CIVL_system at MPItoCIVLTransformer:0.-1-20 "$parfor(int i: 0 ...." inserted by MPItoCIVLTransformer.$parfor MPI_Process before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from civlc.cvl:8.9-20 "<civlc.cvh>"

process p1 (id=1):
  printData at wave1dBad.c:197.5-12 "$assert" called from
  write_frame at wave1dBad.c:211.4-13 "printData" called from
  _gen_main at wave1dBad.c:257.6-17 "write_frame" called from
  _mpi_process at GeneralTransformer:0.-1-20 "_gen_argc, &_gen_a..." inserted by GeneralTransformer.new main function before wave1dBad.c:233.13-17 "argc"

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

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

=== Stats ===
   time (s)            : 3.95
   memory (bytes)      : 650117120
   max process count   : 2
   states              : 496
   states saved        : 294
   state matches       : 0
   transitions         : 495
   trace steps         : 279
   valid calls         : 2118
   provers             : z3, cvc4, cvc3
   prover calls        : 46

=== Result ===
The program MAY NOT be correct.  See CIVLREP/wave1dBad_log.txt
NAME: gausselim.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$NROW$\leq$4,1$\leq$NCOL$\leq$2,1$\leq$NP$\leq$3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (80.7 files/s, 33914.9 lines/s)"
1,C,33,94,293
civl verify -enablePrintf=false  gausselim.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
18s: mem=1326Mb trans=52154 traceSteps=31750 explored=52246 saved=32674 prove=539
33s: mem=1214Mb trans=109968 traceSteps=67365 explored=110350 saved=69677 prove=864
48s: mem=1016Mb trans=174024 traceSteps=106394 explored=174735 saved=110342 prove=1163
63s: mem=822Mb trans=211962 traceSteps=129738 explored=212926 saved=134741 prove=1494
78s: mem=631Mb trans=267140 traceSteps=163748 explored=268444 saved=170226 prove=1629
93s: mem=551Mb trans=323569 traceSteps=198484 explored=325212 saved=206485 prove=1744
108s: mem=706Mb trans=373411 traceSteps=228910 explored=375342 saved=238266 prove=1902

=== Command ===
civl verify -enablePrintf=false gausselim.c 

=== Stats ===
   time (s)            : 114.76
   memory (bytes)      : 627572736
   max process count   : 4
   states              : 408185
   states saved        : 258903
   state matches       : 0
   transitions         : 406073
   trace steps         : 248641
   valid calls         : 1769614
   provers             : z3, cvc4, cvc3
   prover calls        : 1911

=== Result ===
The standard properties hold for all executions.
NAME: matmat{\U}mw.c
CITE: \cite{fevs:2015:web}
TYPE: $\text{M}$
SCALE: {\texttt{1$\leq$M,N,L$\leq$3,1$\leq$NP$\leq$4}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (94.5 files/s, 11909.2 lines/s)"
1,C,11,11,104
civl verify -enablePrintf=false  matmat_mw/matmat_mw.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
18s: mem=1254Mb trans=82974 traceSteps=48509 explored=83643 saved=50633 prove=36

=== Command ===
civl verify -enablePrintf=false matmat_mw/matmat_mw.c 

=== Stats ===
   time (s)            : 17.67
   memory (bytes)      : 1315438592
   max process count   : 5
   states              : 85982
   states saved        : 52037
   state matches       : 90
   transitions         : 85294
   trace steps         : 49852
   valid calls         : 646793
   provers             : z3, cvc4, cvc3
   prover calls        : 36

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