NAME: diffusion1d.c $ ^{c} $
CITE: 
SCALE: {\texttt{NPlin1,3], NSTEPS,NXin1,5]}}
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl diffusion1d_mpi.c -spec diffusion1d_spec.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2453Mb trans=87069 traceSteps=38101 explored=87130 saved=58228 prove=88
34s: mem=3013Mb trans=210230 traceSteps=90834 explored=210384 saved=140072 prove=88

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

=== Stats ===
   time (s)            : 41.54
   memory (bytes)      : 2993684480
   max process count   : 4
   states              : 287405
   states saved        : 193633
   state matches       : 0
   transitions         : 287179
   trace steps         : 124889
   valid calls         : 479109
   provers             : z3, cvc4, cvc3
   prover calls        : 88

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c $ ^{c} $
CITE: 
SCALE: {\texttt{NPX=NPY=2, NSTEPS,NX,NYin1,5]}}
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl diffusion2d_mpi.c -spec diffusion2d_spec.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2013Mb trans=45398 traceSteps=19138 explored=45405 saved=28659 prove=39
34s: mem=2986Mb trans=99668 traceSteps=41525 explored=99681 saved=62850 prove=39
49s: mem=2593Mb trans=162216 traceSteps=66821 explored=162238 saved=102008 prove=39
64s: mem=2392Mb trans=228497 traceSteps=94164 explored=228529 saved=143884 prove=39
79s: mem=2035Mb trans=285789 traceSteps=117748 explored=285829 saved=180040 prove=39
94s: mem=2503Mb trans=350406 traceSteps=143887 explored=350457 saved=220824 prove=39
109s: mem=2924Mb trans=408288 traceSteps=167818 explored=408348 saved=257288 prove=39
124s: mem=3173Mb trans=467092 traceSteps=191704 explored=467161 saved=294267 prove=39
139s: mem=3126Mb trans=533427 traceSteps=218790 explored=533509 saved=336192 prove=39
154s: mem=3137Mb trans=591321 traceSteps=242395 explored=591414 saved=372774 prove=39
169s: mem=3120Mb trans=676705 traceSteps=277673 explored=676821 saved=427118 prove=39

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

=== Stats ===
   time (s)            : 172.31
   memory (bytes)      : 3201826816
   max process count   : 5
   states              : 703630
   states saved        : 444200
   state matches       : 0
   transitions         : 703504
   trace steps         : 288651
   valid calls         : 2114138
   provers             : z3, cvc4, cvc3
   prover calls        : 39

=== Result ===
The standard properties hold for all executions.
NAME: wave1d.c $ ^{c} $
CITE: 
SCALE: {\texttt{NPin1,4], NSTEPS,NXin1,5]}}
civl compare -enablePrintf=false -showAmpleSet -collectHeaps=false -impl wave1d_mpi.c -spec wave1d_spec.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
20s: mem=2451Mb trans=70823 traceSteps=28451 explored=70859 saved=43778 prove=28

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

=== Stats ===
   time (s)            : 31.54
   memory (bytes)      : 3117940736
   max process count   : 5
   states              : 148817
   states saved        : 92357
   state matches       : 0
   transitions         : 148736
   trace steps         : 59359
   valid calls         : 279893
   provers             : z3, cvc4, cvc3
   prover calls        : 28

=== Result ===
The standard properties hold for all executions.
NAME: matmat_mw.c $ ^{c} $
CITE: 
SCALE: {\texttt{NP=5, N=L=M=8}}
cd matmat_mw/ && make
civl compare -collectHeaps=false -enablePrintf=false -showAmpleSet -impl matmat_mw_mpi.c -spec matmat_spec.c 
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl

ample processes at state (id=4780):	2	3	

ample processes at state (id=6329):	1	3	

ample processes at state (id=7601):	1	3	

ample processes at state (id=8873):	1	3	

ample processes at state (id=10145):	1	3	

ample processes at state (id=11417):	1	3	

ample processes at state (id=12689):	1	3	

ample processes at state (id=13961):	1	3	
19s: mem=2451Mb trans=57275 traceSteps=30971 explored=57203 saved=38735 prove=2

ample processes at state (id=248596):	1	2	

ample processes at state (id=249872):	1	2	

ample processes at state (id=251148):	1	2	

ample processes at state (id=252424):	1	2	

ample processes at state (id=253700):	1	2	

ample processes at state (id=254976):	1	2	

ample processes at state (id=256252):	1	2	

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

=== Stats ===
   time (s)            : 31.52
   memory (bytes)      : 2984771584
   max process count   : 4
   states              : 110949
   states saved        : 75033
   state matches       : 163
   transitions         : 111110
   trace steps         : 59757
   valid calls         : 808344
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
NAME: gauss_elim_rowdist.c $ ^{c} $
CITE: 
SCALE: {\texttt{NP=ROW=COL=3}}
civl compare -showAmpleSet -enablePrintf=false -input_mpi_nprocs=3 -spec gausselim_spec.c -impl gausselim_rowdist.c
CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
19s: mem=2455Mb trans=35536 traceSteps=14014 explored=35539 saved=20813 prove=146
34s: mem=3012Mb trans=84593 traceSteps=33327 explored=84600 saved=49655 prove=279
49s: mem=2725Mb trans=135545 traceSteps=53430 explored=135555 saved=79709 prove=398
64s: mem=2505Mb trans=196313 traceSteps=77473 explored=196336 saved=115596 prove=488
79s: mem=2215Mb trans=242948 traceSteps=95747 explored=242974 saved=143839 prove=673

=== Command ===
civl compare -showAmpleSet -enablePrintf=false -input_mpi_nprocs=3 -spec gausselim_spec.c -impl gausselim_rowdist.c 

=== Stats ===
   time (s)            : 88.32
   memory (bytes)      : 2230321152
   max process count   : 4
   states              : 276718
   states saved        : 165354
   state matches       : 0
   transitions         : 276683
   trace steps         : 109000
   valid calls         : 679214
   provers             : z3, cvc4, cvc3
   prover calls        : 787

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