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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2454Mb trans=79020 traceSteps=35520 explored=80246 saved=35521 prove=125
34s: mem=2839Mb trans=190283 traceSteps=84427 explored=193277 saved=84428 prove=125

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

=== Stats ===
   time (s)            : 44.03
   memory (bytes)      : 2734161920
   max process count   : 4
   states              : 285961
   states saved        : 125586
   state matches       : 0
   transitions         : 281860
   trace steps         : 125585
   valid calls         : 1168909
   provers             : z3, cvc4
   prover calls        : 125

=== 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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2451Mb trans=32377 traceSteps=13110 explored=32838 saved=13111 prove=58
34s: mem=3014Mb trans=79348 traceSteps=31812 explored=80470 saved=31813 prove=58
49s: mem=2613Mb trans=133636 traceSteps=53060 explored=135510 saved=53061 prove=58
64s: mem=2313Mb trans=193239 traceSteps=75896 explored=195957 saved=75897 prove=58
79s: mem=2044Mb trans=247600 traceSteps=97470 explored=251033 saved=97471 prove=58
94s: mem=1762Mb trans=294857 traceSteps=116243 explored=298972 saved=116244 prove=58
109s: mem=1512Mb trans=350636 traceSteps=138017 explored=355546 saved=138018 prove=58
124s: mem=1195Mb trans=410773 traceSteps=161459 explored=416479 saved=161460 prove=58
139s: mem=952Mb trans=463198 traceSteps=182108 explored=469645 saved=182109 prove=58
154s: mem=713Mb trans=521880 traceSteps=204835 explored=529171 saved=204836 prove=58
169s: mem=1289Mb trans=578708 traceSteps=227132 explored=586759 saved=227133 prove=58
184s: mem=1904Mb trans=634328 traceSteps=249052 explored=643177 saved=249053 prove=58
199s: mem=2411Mb trans=708710 traceSteps=278171 explored=718404 saved=278172 prove=58

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

=== Stats ===
   time (s)            : 207.89
   memory (bytes)      : 2708471808
   max process count   : 5
   states              : 779098
   states saved        : 301397
   state matches       : 0
   transitions         : 768852
   trace steps         : 301396
   valid calls         : 4273169
   provers             : z3, cvc4
   prover calls        : 58

=== 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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
20s: mem=2462Mb trans=65748 traceSteps=26508 explored=66861 saved=26509 prove=40

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

=== Stats ===
   time (s)            : 31.58
   memory (bytes)      : 3152019456
   max process count   : 5
   states              : 143385
   states saved        : 56330
   state matches       : 0
   transitions         : 141144
   trace steps         : 56329
   valid calls         : 656435
   provers             : z3, cvc4
   prover calls        : 40

=== 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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2452Mb trans=27347 traceSteps=14315 explored=27491 saved=14221 prove=2
34s: mem=2306Mb trans=56551 traceSteps=29187 explored=56857 saved=28946 prove=2
49s: mem=2124Mb trans=86498 traceSteps=44427 explored=86965 saved=44035 prove=2
64s: mem=1963Mb trans=115881 traceSteps=59407 explored=116501 saved=58849 prove=2
79s: mem=1749Mb trans=145318 traceSteps=74383 explored=146109 saved=73670 prove=2
94s: mem=1566Mb trans=174788 traceSteps=89373 explored=175735 saved=88502 prove=2
109s: mem=1361Mb trans=203744 traceSteps=104179 explored=204852 saved=103149 prove=2
124s: mem=1184Mb trans=233263 traceSteps=119160 explored=234532 saved=117978 prove=2
139s: mem=999Mb trans=261720 traceSteps=133742 explored=263139 saved=132411 prove=2
154s: mem=815Mb trans=290634 traceSteps=148441 explored=292204 saved=146947 prove=2
169s: mem=666Mb trans=318774 traceSteps=162894 explored=320502 saved=161248 prove=2
184s: mem=534Mb trans=346890 traceSteps=177273 explored=348772 saved=175473 prove=2
199s: mem=435Mb trans=374929 traceSteps=191635 explored=376964 saved=189676 prove=2
214s: mem=393Mb trans=402981 traceSteps=205981 explored=405171 saved=203869 prove=2
229s: mem=399Mb trans=431040 traceSteps=220351 explored=433375 saved=218081 prove=2
244s: mem=396Mb trans=459362 traceSteps=234753 explored=461849 saved=232334 prove=2
259s: mem=393Mb trans=487108 traceSteps=248961 explored=489745 saved=246391 prove=2
274s: mem=393Mb trans=514823 traceSteps=263145 explored=517601 saved=260411 prove=2
289s: mem=396Mb trans=542615 traceSteps=277379 explored=545551 saved=274500 prove=2
304s: mem=389Mb trans=570211 traceSteps=291517 explored=573281 saved=288487 prove=2
319s: mem=392Mb trans=598753 traceSteps=306014 explored=601980 saved=302831 prove=2
334s: mem=403Mb trans=626377 traceSteps=320152 explored=629740 saved=316810 prove=2
349s: mem=406Mb trans=654362 traceSteps=334436 explored=657881 saved=330946 prove=2

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

=== Stats ===
   time (s)            : 357.48
   memory (bytes)      : 413138944
   max process count   : 6
   states              : 673808
   states saved        : 339032
   state matches       : 3599
   transitions         : 670230
   trace steps         : 342630
   valid calls         : 8327517
   provers             : z3, cvc4
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
NAME: gauss_elim.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.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2452Mb trans=33918 traceSteps=16245 explored=34109 saved=16246 prove=248

ample processes at state 30023:	1	3	

ample processes at state 30025:	1	3	

ample processes at state 30027:	1	3	

ample processes at state 30045:	1	3	

ample processes at state 30047:	1	3	

ample processes at state 30049:	1	3	

ample processes at state 30848:	1	3	

ample processes at state 30850:	1	3	

ample processes at state 30852:	1	3	

ample processes at state 30870:	1	3	

ample processes at state 30872:	1	3	

ample processes at state 30874:	1	3	

ample processes at state 32323:	1	3	

ample processes at state 32325:	1	3	

ample processes at state 32327:	1	3	

ample processes at state 32345:	1	3	

ample processes at state 32347:	1	3	

ample processes at state 32349:	1	3	

ample processes at state 33148:	1	3	

ample processes at state 33150:	1	3	

ample processes at state 33152:	1	3	

ample processes at state 33170:	1	3	

ample processes at state 33172:	1	3	

ample processes at state 33174:	1	3	

ample processes at state 34809:	1	3	

ample processes at state 34811:	1	3	

ample processes at state 34813:	1	3	

ample processes at state 34831:	1	3	

ample processes at state 34833:	1	3	

ample processes at state 34835:	1	3	

ample processes at state 35634:	1	3	

ample processes at state 35636:	1	3	

ample processes at state 35638:	1	3	

ample processes at state 35656:	1	3	

ample processes at state 35658:	1	3	

ample processes at state 35660:	1	3	

ample processes at state 37109:	1	3	

ample processes at state 37111:	1	3	

ample processes at state 37113:	1	3	

ample processes at state 37131:	1	3	

ample processes at state 37133:	1	3	

ample processes at state 37135:	1	3	
34s: mem=2214Mb trans=78999 traceSteps=37504 explored=79501 saved=37466 prove=445

ample processes at state 37934:	1	3	

ample processes at state 37936:	1	3	

ample processes at state 37938:	1	3	

ample processes at state 37956:	1	3	

ample processes at state 37958:	1	3	

ample processes at state 37960:	1	3	

ample processes at state 39831:	1	3	

ample processes at state 39833:	1	3	

ample processes at state 39835:	1	3	

ample processes at state 39853:	1	3	

ample processes at state 39855:	1	3	

ample processes at state 39857:	1	3	

ample processes at state 41355:	1	3	

ample processes at state 41357:	1	3	

ample processes at state 41359:	1	3	

ample processes at state 41377:	1	3	

ample processes at state 41379:	1	3	

ample processes at state 41381:	1	3	

ample processes at state 43065:	1	3	

ample processes at state 43067:	1	3	

ample processes at state 43069:	1	3	

ample processes at state 43087:	1	3	

ample processes at state 43089:	1	3	

ample processes at state 43091:	1	3	

ample processes at state 44589:	1	3	

ample processes at state 44591:	1	3	

ample processes at state 44593:	1	3	

ample processes at state 44611:	1	3	

ample processes at state 44613:	1	3	

ample processes at state 44615:	1	3	
49s: mem=1965Mb trans=124894 traceSteps=59044 explored=125708 saved=58973 prove=668

ample processes at state 65716:	1	3	

ample processes at state 65718:	1	3	

ample processes at state 65720:	1	3	

ample processes at state 65738:	1	3	

ample processes at state 65740:	1	3	

ample processes at state 65742:	1	3	

ample processes at state 66541:	1	3	

ample processes at state 66543:	1	3	

ample processes at state 66545:	1	3	

ample processes at state 66563:	1	3	

ample processes at state 66565:	1	3	

ample processes at state 66567:	1	3	

ample processes at state 68065:	1	3	

ample processes at state 68067:	1	3	

ample processes at state 68069:	1	3	

ample processes at state 68087:	1	3	

ample processes at state 68089:	1	3	

ample processes at state 68091:	1	3	

ample processes at state 68890:	1	3	

ample processes at state 68892:	1	3	

ample processes at state 68894:	1	3	

ample processes at state 68912:	1	3	

ample processes at state 68914:	1	3	

ample processes at state 68916:	1	3	

ample processes at state 70836:	1	3	

ample processes at state 70838:	1	3	

ample processes at state 70840:	1	3	

ample processes at state 70858:	1	3	

ample processes at state 70860:	1	3	

ample processes at state 70862:	1	3	

ample processes at state 72409:	1	3	

ample processes at state 72411:	1	3	

ample processes at state 72413:	1	3	

ample processes at state 72431:	1	3	

ample processes at state 72433:	1	3	

ample processes at state 72435:	1	3	
64s: mem=1687Mb trans=173511 traceSteps=81893 explored=174696 saved=81786 prove=842

ample processes at state 84845:	1	3	

ample processes at state 84847:	1	3	

ample processes at state 84849:	1	3	

ample processes at state 84867:	1	3	

ample processes at state 84869:	1	3	

ample processes at state 84871:	1	3	

ample processes at state 85670:	1	3	

ample processes at state 85672:	1	3	

ample processes at state 85674:	1	3	

ample processes at state 85692:	1	3	

ample processes at state 85694:	1	3	

ample processes at state 85696:	1	3	

ample processes at state 87614:	1	3	

ample processes at state 87616:	1	3	

ample processes at state 87618:	1	3	

ample processes at state 87636:	1	3	

ample processes at state 87638:	1	3	

ample processes at state 87640:	1	3	

ample processes at state 90768:	1	3	

ample processes at state 90770:	1	3	

ample processes at state 90772:	1	3	

ample processes at state 90790:	1	3	

ample processes at state 90792:	1	3	

ample processes at state 90794:	1	3	

ample processes at state 91593:	1	3	

ample processes at state 91595:	1	3	

ample processes at state 91597:	1	3	

ample processes at state 91615:	1	3	

ample processes at state 91617:	1	3	

ample processes at state 91619:	1	3	

ample processes at state 92851:	1	3	

ample processes at state 92853:	1	3	

ample processes at state 92855:	1	3	

ample processes at state 92873:	1	3	

ample processes at state 92875:	1	3	

ample processes at state 92877:	1	3	

ample processes at state 93676:	1	3	

ample processes at state 93678:	1	3	

ample processes at state 93680:	1	3	

ample processes at state 93698:	1	3	

ample processes at state 93700:	1	3	

ample processes at state 93702:	1	3	

ample processes at state 95004:	1	3	

ample processes at state 95006:	1	3	

ample processes at state 95008:	1	3	

ample processes at state 95026:	1	3	

ample processes at state 95028:	1	3	

ample processes at state 95030:	1	3	

ample processes at state 95829:	1	3	

ample processes at state 95831:	1	3	

ample processes at state 95833:	1	3	

ample processes at state 95851:	1	3	

ample processes at state 95853:	1	3	

ample processes at state 95855:	1	3	

ample processes at state 97087:	1	3	

ample processes at state 97089:	1	3	

ample processes at state 97091:	1	3	

ample processes at state 97109:	1	3	

ample processes at state 97111:	1	3	

ample processes at state 97113:	1	3	

ample processes at state 97912:	1	3	

ample processes at state 97914:	1	3	

ample processes at state 97916:	1	3	

ample processes at state 97934:	1	3	

ample processes at state 97936:	1	3	

ample processes at state 97938:	1	3	

ample processes at state 99802:	1	3	

ample processes at state 99804:	1	3	

ample processes at state 99806:	1	3	

ample processes at state 99824:	1	3	

ample processes at state 99826:	1	3	

ample processes at state 99828:	1	3	

ample processes at state 101109:	1	3	

ample processes at state 101111:	1	3	

ample processes at state 101113:	1	3	

ample processes at state 101131:	1	3	

ample processes at state 101133:	1	3	

ample processes at state 101135:	1	3	

ample processes at state 102486:	1	3	

ample processes at state 102488:	1	3	

ample processes at state 102490:	1	3	

ample processes at state 102508:	1	3	

ample processes at state 102510:	1	3	

ample processes at state 102512:	1	3	

ample processes at state 103793:	1	3	

ample processes at state 103795:	1	3	

ample processes at state 103797:	1	3	

ample processes at state 103815:	1	3	

ample processes at state 103817:	1	3	

ample processes at state 103819:	1	3	
79s: mem=1362Mb trans=227267 traceSteps=106785 explored=228860 saved=106588 prove=970

ample processes at state 109083:	1	3	

ample processes at state 109085:	1	3	

ample processes at state 109087:	1	3	

ample processes at state 109105:	1	3	

ample processes at state 109107:	1	3	

ample processes at state 109109:	1	3	

ample processes at state 109908:	1	3	

ample processes at state 109910:	1	3	

ample processes at state 109912:	1	3	

ample processes at state 109930:	1	3	

ample processes at state 109932:	1	3	

ample processes at state 109934:	1	3	

ample processes at state 111215:	1	3	

ample processes at state 111217:	1	3	

ample processes at state 111219:	1	3	

ample processes at state 111237:	1	3	

ample processes at state 111239:	1	3	

ample processes at state 111241:	1	3	

ample processes at state 112040:	1	3	

ample processes at state 112042:	1	3	

ample processes at state 112044:	1	3	

ample processes at state 112062:	1	3	

ample processes at state 112064:	1	3	

ample processes at state 112066:	1	3	

ample processes at state 113979:	1	3	

ample processes at state 113981:	1	3	

ample processes at state 113983:	1	3	

ample processes at state 114001:	1	3	

ample processes at state 114003:	1	3	

ample processes at state 114005:	1	3	

ample processes at state 115335:	1	3	

ample processes at state 115337:	1	3	

ample processes at state 115339:	1	3	

ample processes at state 115357:	1	3	

ample processes at state 115359:	1	3	

ample processes at state 115361:	1	3	

ample processes at state 119277:	1	3	

ample processes at state 119279:	1	3	

ample processes at state 119281:	1	3	

ample processes at state 119299:	1	3	

ample processes at state 119301:	1	3	

ample processes at state 119303:	1	3	

ample processes at state 120102:	1	3	

ample processes at state 120104:	1	3	

ample processes at state 120106:	1	3	

ample processes at state 120124:	1	3	

ample processes at state 120126:	1	3	

ample processes at state 120128:	1	3	

ample processes at state 122039:	1	3	

ample processes at state 122041:	1	3	

ample processes at state 122043:	1	3	

ample processes at state 122061:	1	3	

ample processes at state 122063:	1	3	

ample processes at state 122065:	1	3	

ample processes at state 124926:	1	3	

ample processes at state 124928:	1	3	

ample processes at state 124930:	1	3	

ample processes at state 124948:	1	3	

ample processes at state 124950:	1	3	

ample processes at state 124952:	1	3	

ample processes at state 125751:	1	3	

ample processes at state 125753:	1	3	

ample processes at state 125755:	1	3	

ample processes at state 125773:	1	3	

ample processes at state 125775:	1	3	

ample processes at state 125777:	1	3	

ample processes at state 126646:	1	3	

ample processes at state 126648:	1	3	

ample processes at state 126650:	1	3	

ample processes at state 126668:	1	3	

ample processes at state 126670:	1	3	

ample processes at state 126672:	1	3	

ample processes at state 127471:	1	3	

ample processes at state 127473:	1	3	

ample processes at state 127475:	1	3	

ample processes at state 127493:	1	3	

ample processes at state 127495:	1	3	

ample processes at state 127497:	1	3	

ample processes at state 129138:	1	3	

ample processes at state 129140:	1	3	

ample processes at state 129142:	1	3	

ample processes at state 129160:	1	3	

ample processes at state 129162:	1	3	

ample processes at state 129164:	1	3	

ample processes at state 130012:	1	3	

ample processes at state 130014:	1	3	

ample processes at state 130016:	1	3	

ample processes at state 130034:	1	3	

ample processes at state 130036:	1	3	

ample processes at state 130038:	1	3	

ample processes at state 131677:	1	3	

ample processes at state 131679:	1	3	

ample processes at state 131681:	1	3	

ample processes at state 131699:	1	3	

ample processes at state 131701:	1	3	

ample processes at state 131703:	1	3	
94s: mem=1114Mb trans=284857 traceSteps=133204 explored=286906 saved=132911 prove=1045

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

=== Stats ===
   time (s)            : 93.57
   memory (bytes)      : 1168113664
   max process count   : 4
   states              : 287641
   states saved        : 133200
   state matches       : 294
   transitions         : 285584
   trace steps         : 133493
   valid calls         : 1847940
   provers             : z3, cvc4
   prover calls        : 1045

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