NAME: diffusion1d.c $ ^{c} $
CITE: \cite{LLNL:MPI:URL}
SCALE: {\text{1<=NP<=3, 1<=NSTEPS,NX<=5}}
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl diffusion1d_mpi.c -spec diffusion1d_spec.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2447Mb trans=77446 traceSteps=35101 explored=78137 saved=35103 prove=241
33s: mem=2214Mb trans=189700 traceSteps=84905 explored=191406 saved=84906 prove=241

=== Command ===
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl diffusion1d_mpi.c -spec diffusion1d_spec.c 

=== Stats ===
   time (s)            : 44.29
   memory (bytes)      : 2061500416
   max process count   : 4
   states              : 296974
   states saved        : 131777
   state matches       : 0
   transitions         : 294458
   trace steps         : 131776
   valid calls         : 1263291
   provers             : cvc4, z3, cvc3
   prover calls        : 241

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c $ ^{c} $
CITE: \cite{LLNL:MPI:URL}
SCALE: {\text{NPX=NPY=2, 1<=NSTEPS,NX,NY<=5}}
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl diffusion2d_mpi.c -spec diffusion2d_spec.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2446Mb trans=35894 traceSteps=14767 explored=36162 saved=14768 prove=58
33s: mem=2323Mb trans=83957 traceSteps=34198 explored=84581 saved=34199 prove=58
48s: mem=2044Mb trans=136428 traceSteps=55323 explored=137445 saved=55324 prove=58
63s: mem=1756Mb trans=196343 traceSteps=78833 explored=197805 saved=78834 prove=58
78s: mem=1567Mb trans=250878 traceSteps=100885 explored=252730 saved=100886 prove=58
93s: mem=1323Mb trans=297630 traceSteps=119862 explored=299838 saved=119863 prove=58
108s: mem=1090Mb trans=351096 traceSteps=141375 explored=353719 saved=141376 prove=58
123s: mem=855Mb trans=411718 traceSteps=165421 explored=414773 saved=165422 prove=58
138s: mem=646Mb trans=465322 traceSteps=187012 explored=468785 saved=187013 prove=58
153s: mem=537Mb trans=519654 traceSteps=208660 explored=523545 saved=208661 prove=58
168s: mem=636Mb trans=584341 traceSteps=234272 explored=588694 saved=234273 prove=58
183s: mem=1224Mb trans=633847 traceSteps=254320 explored=638596 saved=254321 prove=58
198s: mem=1757Mb trans=703184 traceSteps=281736 explored=708410 saved=281737 prove=58

=== Command ===
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl diffusion2d_mpi.c -spec diffusion2d_spec.c 

=== Stats ===
   time (s)            : 209.92
   memory (bytes)      : 2223505408
   max process count   : 5
   states              : 788986
   states saved        : 312980
   state matches       : 0
   transitions         : 783300
   trace steps         : 312979
   valid calls         : 4554091
   provers             : cvc4, z3, cvc3
   prover calls        : 58

=== Result ===
The standard properties hold for all executions.
NAME: wave1d.c $ ^{c} $
CITE: \cite{LLNL:MPI:URL}
SCALE: {\text{1<=NP<=4, 1<=NSTEPS,NX<=5}}
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl wave1d_mpi.c -spec wave1d_spec.c
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2454Mb trans=67001 traceSteps=28305 explored=67573 saved=28307 prove=41

=== Command ===
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl wave1d_mpi.c -spec wave1d_spec.c 

=== Stats ===
   time (s)            : 31.05
   memory (bytes)      : 2979004416
   max process count   : 5
   states              : 144985
   states saved        : 60503
   state matches       : 0
   transitions         : 143824
   trace steps         : 60502
   valid calls         : 710344
   provers             : cvc4, z3, cvc3
   prover calls        : 41

=== Result ===
The standard properties hold for all executions.
NAME: matmat_mw.c $ ^{c} $
CITE: \cite{LLNL:MPI:URL}
SCALE: {\text{2<=NP<=4, 1<=N,L,M<=3}}
cd matmat_mw/ && make
civl compare -collectHeaps=false -enablePrintf=false -showAmpleSet -impl matmat_mw_mpi.c -spec matmat_spec.c 
CIVL v1.7+ of 2016-03-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2446Mb trans=96710 traceSteps=39234 explored=97481 saved=39163 prove=35

=== Command ===
civl compare -collectHeaps=false -enablePrintf=false -showAmpleSet -impl matmat_mw_mpi.c -spec matmat_spec.c 

=== Stats ===
   time (s)            : 20.03
   memory (bytes)      : 2565341184
   max process count   : 5
   states              : 119872
   states saved        : 47856
   state matches       : 90
   transitions         : 118917
   trace steps         : 47945
   valid calls         : 877266
   provers             : cvc4, z3, cvc3
   prover calls        : 35

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