NAME: matmat_mw.c
CITE: \cite{LLNL:MPI:URL}
SCALE: {\texttt{NP=3, N=L=M=4}}
civl verify -enablePrintf=false -input_mpi_nprocs=5 -inputN=8 -inputL=8 -inputM=8 matmat_mw.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=1420Mb trans=19497 traceSteps=9990 explored=19607 saved=9920 prove=2
34s: mem=2451Mb trans=39152 traceSteps=20035 explored=39371 saved=19869 prove=2
49s: mem=2306Mb trans=59123 traceSteps=30170 explored=59451 saved=29904 prove=2
64s: mem=2124Mb trans=79333 traceSteps=40392 explored=79767 saved=40018 prove=2
79s: mem=1962Mb trans=99006 traceSteps=50506 explored=99548 saved=50034 prove=2
94s: mem=1817Mb trans=118607 traceSteps=60492 explored=119257 saved=59909 prove=2
109s: mem=1685Mb trans=138337 traceSteps=70498 explored=139102 saved=69811 prove=2
124s: mem=1566Mb trans=158164 traceSteps=80606 explored=159034 saved=79817 prove=2
139s: mem=1444Mb trans=177600 traceSteps=90537 explored=178574 saved=89640 prove=2
154s: mem=1274Mb trans=197342 traceSteps=100573 explored=198424 saved=99566 prove=2
169s: mem=1123Mb trans=217270 traceSteps=110721 explored=218460 saved=109614 prove=2
184s: mem=999Mb trans=236916 traceSteps=120689 explored=238216 saved=119480 prove=2
199s: mem=855Mb trans=256347 traceSteps=130672 explored=257741 saved=129350 prove=2
214s: mem=739Mb trans=275710 traceSteps=140534 explored=277213 saved=139108 prove=2
229s: mem=623Mb trans=295016 traceSteps=150395 explored=296618 saved=148861 prove=2
244s: mem=530Mb trans=314131 traceSteps=160210 explored=315841 saved=158575 prove=2
259s: mem=452Mb trans=333253 traceSteps=169985 explored=335073 saved=168246 prove=2
274s: mem=401Mb trans=352247 traceSteps=179711 explored=354165 saved=177864 prove=2
289s: mem=383Mb trans=371135 traceSteps=189380 explored=373159 saved=187429 prove=2
304s: mem=383Mb trans=390042 traceSteps=199053 explored=392173 saved=197001 prove=2
319s: mem=383Mb trans=409113 traceSteps=208774 explored=411348 saved=206615 prove=2
334s: mem=395Mb trans=427930 traceSteps=218487 explored=430264 saved=216229 prove=2
349s: mem=383Mb trans=447345 traceSteps=228307 explored=449780 saved=225937 prove=2
364s: mem=385Mb trans=466511 traceSteps=238065 explored=469046 saved=235591 prove=2
379s: mem=390Mb trans=485007 traceSteps=247571 explored=487644 saved=245000 prove=2
394s: mem=399Mb trans=503893 traceSteps=257242 explored=506620 saved=254556 prove=2
409s: mem=385Mb trans=522758 traceSteps=266932 explored=525593 saved=264142 prove=2
424s: mem=387Mb trans=541887 traceSteps=276670 explored=544822 saved=273776 prove=2
439s: mem=384Mb trans=560581 traceSteps=286312 explored=563605 saved=283314 prove=2
454s: mem=383Mb trans=579728 traceSteps=296037 explored=582857 saved=292939 prove=2
469s: mem=387Mb trans=598976 traceSteps=305817 explored=602202 saved=302611 prove=2
484s: mem=387Mb trans=617631 traceSteps=315374 explored=620965 saved=312074 prove=2
499s: mem=402Mb trans=636439 traceSteps=325002 explored=639874 saved=321600 prove=2
514s: mem=401Mb trans=655400 traceSteps=334676 explored=658923 saved=331158 prove=2

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs=5 -inputN=8 -inputL=8 -inputM=8 matmat_mw.c 

=== Stats ===
   time (s)            : 523.4
   memory (bytes)      : 411566080
   max process count   : 6
   states              : 671592
   states saved        : 337587
   state matches       : 3599
   transitions         : 668015
   trace steps         : 341185
   valid calls         : 8307748
   provers             : cvc4, z3
   prover calls        : 2

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