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.02 s (61.4 files/s, 12946.3 lines/s)"
1,C,21,25,165
civl verify -enablePrintf=false  diffusion1d.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
17s: mem=1326Mb steps=43943 trans=26528 seen=26529 saved=27433 prove=282
32s: mem=1137Mb steps=97292 trans=58263 seen=58264 saved=60460 prove=383

=================== Stats ===================
   validCalls          : 452505
   proverCalls         : 399
   memory (bytes)      : 1089994752
   time (s)            : 36.51
   maxProcs            : 4
   statesInstantiated  : 719741
   statesSaved         : 69360
   statesSeen          : 66786
   statesMatched       : 0
   steps               : 111704
   transitions         : 66785

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.02 s (63.2 files/s, 23258.9 lines/s)"
1,C,27,66,275
civl verify -enablePrintf=false  diffusion2d.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
18s: mem=1303Mb steps=35184 trans=23157 seen=23158 saved=24069 prove=115
33s: mem=1109Mb steps=70389 trans=45933 seen=45934 saved=47803 prove=166
48s: mem=911Mb steps=104745 trans=67696 seen=67697 saved=70411 prove=221
63s: mem=741Mb steps=132712 trans=85261 seen=85262 saved=88741 prove=261
78s: mem=593Mb steps=159059 trans=101693 seen=101693 saved=105862 prove=281
93s: mem=479Mb steps=181560 trans=115573 seen=115574 saved=120298 prove=293
108s: mem=464Mb steps=214282 trans=136413 seen=136414 saved=141951 prove=356
123s: mem=483Mb steps=240595 trans=152964 seen=152965 saved=159199 prove=388
138s: mem=450Mb steps=261736 trans=165975 seen=165976 saved=172712 prove=400
153s: mem=465Mb steps=285772 trans=181166 seen=181167 saved=188541 prove=420
168s: mem=573Mb steps=311914 trans=197839 seen=197840 saved=205825 prove=470
183s: mem=498Mb steps=338080 trans=214197 seen=214198 saved=222842 prove=502
198s: mem=650Mb steps=359915 trans=227954 seen=227955 saved=237150 prove=530
213s: mem=527Mb steps=377702 trans=239069 seen=239070 saved=248715 prove=538
228s: mem=546Mb steps=397719 trans=251531 seen=251532 saved=261659 prove=550
243s: mem=519Mb steps=420353 trans=266037 seen=266038 saved=276676 prove=587
258s: mem=570Mb steps=445498 trans=281829 seen=281829 saved=293088 prove=615
273s: mem=537Mb steps=464031 trans=293418 seen=293419 saved=305128 prove=639
288s: mem=514Mb steps=483838 trans=305762 seen=305762 saved=317938 prove=651
303s: mem=807Mb steps=501192 trans=316740 seen=316741 saved=329339 prove=671
318s: mem=747Mb steps=515151 trans=325330 seen=325331 saved=338258 prove=671

=================== Stats ===================
   validCalls          : 2597686
   proverCalls         : 671
   memory (bytes)      : 747634688
   time (s)            : 323.49
   maxProcs            : 5
   statesInstantiated  : 3700337
   statesSaved         : 339974
   statesSeen          : 326995
   statesMatched       : 0
   steps               : 517959
   transitions         : 326994

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 (69.7 files/s, 9549.0 lines/s)"
1,C,10,25,102
civl verify -enablePrintf=false  mpi_prime.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
18s: mem=611Mb steps=20390 trans=10411 seen=10412 saved=10825 prove=750

=================== Stats ===================
   validCalls          : 64634
   proverCalls         : 766
   memory (bytes)      : 641204224
   time (s)            : 17.52
   maxProcs            : 5
   statesInstantiated  : 117145
   statesSaved         : 11221
   statesSeen          : 10796
   statesMatched       : 0
   steps               : 21135
   transitions         : 10795

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.02 s (63.2 files/s, 10621.5 lines/s)"
1,C,11,38,119
civl verify -enablePrintf=false  mpi_pi_send.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
17s: mem=849Mb steps=15233 trans=8722 seen=8723 saved=9013 prove=701
32s: mem=755Mb steps=27554 trans=15729 seen=15730 saved=16235 prove=1346
47s: mem=684Mb steps=41877 trans=23896 seen=23897 saved=24648 prove=2069
62s: mem=609Mb steps=55948 trans=31925 seen=31926 saved=32921 prove=2793
77s: mem=543Mb steps=69429 trans=39616 seen=39617 saved=40849 prove=3504
92s: mem=483Mb steps=82491 trans=47077 seen=47078 saved=48536 prove=4184
107s: mem=434Mb steps=96203 trans=54910 seen=54911 saved=56607 prove=4889
122s: mem=426Mb steps=109676 trans=62615 seen=62616 saved=64548 prove=5588

=================== Stats ===================
   validCalls          : 367307
   proverCalls         : 5798
   memory (bytes)      : 432537600
   time (s)            : 126.65
   maxProcs            : 3
   statesInstantiated  : 664633
   statesSaved         : 67292
   statesSeen          : 65283
   statesMatched       : 0
   steps               : 114318
   transitions         : 65282

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.02 s (65.3 files/s, 5617.2 lines/s)"
1,C,7,12,67
civl verify -enablePrintf=false  sum_array.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
17s: mem=1325Mb steps=57132 trans=35735 seen=35386 saved=37271 prove=372

=================== Stats ===================
   validCalls          : 492299
   proverCalls         : 409
   memory (bytes)      : 1323827200
   time (s)            : 23.71
   maxProcs            : 6
   statesInstantiated  : 469053
   statesSaved         : 50605
   statesSeen          : 47998
   statesMatched       : 580
   steps               : 76899
   transitions         : 48577

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.02 s (66.4 files/s, 18049.2 lines/s)"
1,C,44,34,194
civl verify -enablePrintf=false  wave1d.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
18s: mem=1322Mb steps=46630 trans=28222 seen=28223 saved=29748 prove=219
33s: mem=1131Mb steps=88813 trans=53917 seen=53918 saved=56906 prove=319

=================== Stats ===================
   validCalls          : 434780
   proverCalls         : 335
   memory (bytes)      : 1117257728
   time (s)            : 36.6
   maxProcs            : 5
   statesInstantiated  : 681001
   statesSaved         : 64268
   statesSeen          : 60883
   statesMatched       : 0
   steps               : 100456
   transitions         : 60882

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 (68.9 files/s, 19017.4 lines/s)"
1,C,44,40,192
civl verify -enablePrintf=false  wave1dBad.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
Error: disagreement at time 2 position 0: saw -4*(X11[1]*(X7^4))+5*(X11[0]*(X7^4))+3*(X11[1]*(X7^2))+-6*(X11[0]*(X7^2))+V0[0]*X7^2+X11[0], expected -4*(X11[1]*(X7^4))+5*(X11[0]*(X7^4))+3*(X11[1]*(X7^2))+-6*(X11[0]*(X7^2))+X11[0]
Error 0 encountered at depth 498:
CIVL execution error in p1(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Cannot prove assertion holds: $assert (((oracle)[(time+1)])[((first+i)+1)]==*((buf+i)))
  Path condition: (0 < X7) && (0 <= SIZEOF_REAL+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
  Assertion: 0 == V0[0]*(X7^2)

at wave1dBad.c:196.5-192 "$assert (oracle[time +  ... ]".
State -1:12561
| Path condition
| | (0 < X7) && (0 <= SIZEOF_REAL+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 3:
| | | | | | 0: (__gbarrier__[1])<__gbarrier__<2,(process[2])<p1,p2>,(boolean[2])<false,false>,0>>
| | | | | objects of malloc 5:
| | | | | | 0: (__gcomm__[1])<__gcomm__<2,(boolean[2])<true,true>,(__queue__[2][2])<(__queue__[2])<__queue__<0,(__message__[0])>>,__queue__<1,(__message__[1])<__message__<0,1,1,inject(8,(real[1])<X11[1]*(X7^2)+-2*(X11[0]*(X7^2))+X11[0]>),SIZEOF_REAL>>>>,(__queue__[2])<__queue__<0,(__message__[0])>>,__queue__<0,(__message__[0])>>>>>>
| | | | | | 1: (__gcomm__[1])<__gcomm__<2,(boolean[2])<true,true>,(__queue__[2][2])<(__queue__[2])<__queue__<0,(__message__[0])>>,__queue__<0,(__message__[0])>>>,(__queue__[2])<__queue__<0,(__message__[0])>>,__queue__<0,(__message__[0])>>>>>>
| | | | _time_count_var = 0
| | | | CIVL_argc = X3
| | | | CIVL_argv = X4
| | | | NXB = 5
| | | | nx = 2
| | | | c = X7
| | | | NSTEPSB = 5
| | | | nsteps = 3
| | | | wstep = 1
| | | | u_init = X11
| | | | _NPROCS = 2
| | | | _NPROCS_LOWER_BOUND = 1
| | | | _NPROCS_UPPER_BOUND = 4
| | | | GCOMM_WORLD = CMPI_Gcomm<&<d0>heap<5,0>[0],&<d0>heap<5,1>[0],&<d0>heap<3,0>[0]>
| | dyscope d3 (id=1, parent=d0, static=45)
| | | variables
| | | | $mpi__procs = (process[2])<p1,p2>
| | dyscope d6 (id=2, parent=d5, static=65)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0 at wave1dBad.c:163.2-55 "u_prev = (double *) ... )":
| | | | | | 0: (real[3])<0,-4*(X11[1]*(X7^4))+5*(X11[0]*(X7^4))+3*(X11[1]*(X7^2))+-6*(X11[0]*(X7^2))+V0[0]*X7^2+X11[0],0>
| | | | | objects of malloc 1 at wave1dBad.c:165.2-55 "u_curr = (double *) ... )":
| | | | | | 0: (real[3])<0,X11[0],X11[1]>
| | | | | objects of malloc 2 at wave1dBad.c:167.2-55 "u_next = (double *) ... )":
| | | | | | 0: V0[1:=X11[1]*X7^2+-2*(X11[0]*(X7^2))+X11[0], 2:=-2*(X11[1]*(X7^2))+X11[0]*X7^2+X11[1]]
| | | | | objects of malloc 4:
| | | | | | 0: (__barrier__[1])<__barrier__<0,&<d0>heap<3,0>[0]>>
| | | | | objects of malloc 6:
| | | | | | 0: (__comm__[1])<__comm__<0,&<d0>heap<5,0>[0]>>
| | | | | | 1: (__comm__[1])<__comm__<0,&<d0>heap<5,1>[0]>>
| | | | _my_status = 1
| | | | MPI_COMM_WORLD = MPI_Comm<&<d6>heap<6,0>[0],&<d6>heap<6,1>[0],&<d6>heap<4,0>[0]>
| | | | $gen_root = d6
| | | | oracle = (real[4][4])<(real[4])<0,X11[0],X11[1],0>,(real[4])<0,X11[0],X11[1],0>,(real[4])<0,X11[1]*X7^2+-2*(X11[0]*(X7^2))+X11[0],-2*(X11[1]*(X7^2))+X11[0]*X7^2+X11[1],0>,V0[3][1:=-4*(X11[1]*(X7^4))+5*(X11[0]*(X7^4))+3*(X11[1]*(X7^2))+-6*(X11[0]*(X7^2))+X11[0], 2:=5*(X11[1]*(X7^4))+-4*(X11[0]*(X7^4))+-6*(X11[1]*(X7^2))+3*(X11[0]*(X7^2))+X11[1]]>
| | | | u_prev = &<d6>heap<2,0>[0]
| | | | u_curr = &<d6>heap<0,0>[0]
| | | | u_next = &<d6>heap<1,0>[0]
| | | | k = X7^2
| | | | nprocs = 2
| | | | nxl = 1
| | | | rank = 0
| | | | first = 0
| | | | left = -3
| | | | right = 1
| | dyscope d5 (id=3, parent=d0, static=44)
| | | variables
| | | | $mpi__rank = 0
| | dyscope d12 (id=4, parent=d11, static=81)
| | | variables
| | | | _argv = (pointer[10])<&<d0>CIVL_argv[0][0],&<d0>CIVL_argv[1][0],&<d0>CIVL_argv[2][0],&<d0>CIVL_argv[3][0],&<d0>CIVL_argv[4][0],&<d0>CIVL_argv[5][0],&<d0>CIVL_argv[6][0],&<d0>CIVL_argv[7][0],&<d0>CIVL_argv[8][0],&<d0>CIVL_argv[9][0]>
| | | | argv = &<d12>_argv[0]
| | | | iter = 2
| | dyscope d11 (id=5, parent=d6, static=73)
| | | variables
| | dyscope d34 (id=6, parent=d618, static=78)
| | | variables
| | | | buf = V1
| | | | status = V2
| | | | _anon_12 = "\n======= Time %d =======\n"
| | | | _anon_13 = NULL
| | dyscope d618 (id=7, parent=d6, static=71)
| | | variables
| | | | time = 2
| | dyscope d36 (id=8, parent=d620, static=77)
| | | variables
| | | | i = 0
| | | | _anon_9 = "u_curr[%d]=%8.8f   "
| | | | _anon_10 = "Error: disagreement at time %d position %d: saw %lf, expected %lf"
| | | | _anon_11 = NULL
| | dyscope d620 (id=9, parent=d6, static=70)
| | | variables
| | | | time = 2
| | | | first = 0
| | | | length = 1
| | | | buf = &<d6>heap<0,0>[1]
| | dyscope d8 (id=10, parent=d7, static=65)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0 at wave1dBad.c:163.2-55 "u_prev = (double *) ... )":
| | | | | | 0: (real[3])<0,X11[1],0>
| | | | | objects of malloc 1 at wave1dBad.c:165.2-55 "u_curr = (double *) ... )":
| | | | | | 0: (real[3])<X11[0],X11[1],0>
| | | | | objects of malloc 2 at wave1dBad.c:167.2-55 "u_next = (double *) ... )":
| | | | | | 0: V3[1:=-2*(X11[1]*(X7^2))+X11[0]*X7^2+X11[1]]
| | | | | objects of malloc 4:
| | | | | | 0: (__barrier__[1])<__barrier__<1,&<d0>heap<3,0>[0]>>
| | | | | objects of malloc 6:
| | | | | | 0: (__comm__[1])<__comm__<1,&<d0>heap<5,0>[0]>>
| | | | | | 1: (__comm__[1])<__comm__<1,&<d0>heap<5,1>[0]>>
| | | | _my_status = 1
| | | | MPI_COMM_WORLD = MPI_Comm<&<d8>heap<6,0>[0],&<d8>heap<6,1>[0],&<d8>heap<4,0>[0]>
| | | | $gen_root = d8
| | | | oracle = V4
| | | | u_prev = &<d8>heap<1,0>[0]
| | | | u_curr = &<d8>heap<2,0>[0]
| | | | u_next = &<d8>heap<0,0>[0]
| | | | k = X7^2
| | | | nprocs = 2
| | | | nxl = 1
| | | | rank = 1
| | | | first = 1
| | | | left = 0
| | | | right = -3
| | dyscope d7 (id=11, parent=d0, static=44)
| | | variables
| | | | $mpi__rank = 1
| | dyscope d48 (id=12, parent=d47, static=81)
| | | variables
| | | | _argv = (pointer[10])<&<d0>CIVL_argv[0][0],&<d0>CIVL_argv[1][0],&<d0>CIVL_argv[2][0],&<d0>CIVL_argv[3][0],&<d0>CIVL_argv[4][0],&<d0>CIVL_argv[5][0],&<d0>CIVL_argv[6][0],&<d0>CIVL_argv[7][0],&<d0>CIVL_argv[8][0],&<d0>CIVL_argv[9][0]>
| | | | argv = &<d48>_argv[0]
| | | | iter = 1
| | dyscope d47 (id=13, parent=d8, static=73)
| | | variables
| | dyscope d104 (id=14, parent=d8, static=72)
| | | variables
| | dyscope d106 (id=15, parent=d345, static=57)
| | | variables
| | | | curr_status = 1
| | | | _anon_5 = "MPI_Sendrecv() cannot be invoked without MPI_Init() being called before.\n"
| | dyscope d345 (id=16, parent=d0, static=26)
| | | variables
| | | | sendbuf = &<d8>heap<2,0>[1]
| | | | sendcount = 1
| | | | sendtype = 23
| | | | dest = 0
| | | | sendtag = 2
| | | | recvbuf = &<d8>heap<2,0>[2]
| | | | recvcount = 1
| | | | recvtype = 23
| | | | source = -3
| | | | recvtag = 2
| | | | comm = MPI_Comm<&<d8>heap<6,0>[0],&<d8>heap<6,1>[0],&<d8>heap<4,0>[0]>
| | | | status = NULL
| | dyscope d72 (id=17, parent=d71, static=52)
| | | variables
| | | | $sef$0 = NULL
| | dyscope d71 (id=18, parent=d347, static=51)
| | | variables
| | | | curr_status = 1
| | | | _anon_2 = "MPI_Send() cannot be invoked without MPI_Init() being called before.\n"
| | dyscope d347 (id=19, parent=d0, static=23)
| | | variables
| | | | buf = &<d8>heap<2,0>[1]
| | | | count = 1
| | | | datatype = 23
| | | | dest = 0
| | | | tag = 2
| | | | comm = MPI_Comm<&<d8>heap<6,0>[0],&<d8>heap<6,1>[0],&<d8>heap<4,0>[0]>
| | dyscope d350 (id=20, parent=d0, static=34)
| | | variables
| | | | buf = &<d8>heap<2,0>[1]
| | | | count = 1
| | | | datatype = 23
| | | | dest = 0
| | | | tag = 2
| | | | comm = &<d8>heap<6,0>[0]
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=17, MPItoCIVLTransformer:0.-1-20 "$mpi__procs, _NPRO..." inserted by MPItoCIVLTransformer.function call$waitallbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from civlc.cvl:9.9-20 "<civlc.cvh>", dyscope=d3]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=printData, location=211, wave1dBad.c:196.5-12 "$assert", dyscope=d36]
| | | | Frame[function=write_frame, location=220, wave1dBad.c:210.4-13 "printData", dyscope=d34]
| | | | Frame[function=$mpi__main, location=255, wave1dBad.c:263.6-17 "write_frame", dyscope=d12]
| | | | Frame[function=MPI_Process, location=146, MPItoCIVLTransformer:0.-1 "" inserted by MPItoCIVLTransformer.function call $mpi__mainbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from civlc.cvl:9.9-20 "<civlc.cvh>", dyscope=d6]
| | process p2(id=2)
| | | call stack
| | | | Frame[function=CMPI_Send, location=108, civl-mpi.cvl:111.2-8 "return", dyscope=d110]
| | | | Frame[function=MPI_Send, location=44, mpi.cvl:68.9-18 "CMPI_Send", dyscope=d109]
| | | | Frame[function=MPI_Sendrecv, location=60, mpi.cvl:103.2-10 "MPI_Send", dyscope=d106]
| | | | Frame[function=exchange, location=232, wave1dBad.c:226.2-14 "MPI_Sendrecv", dyscope=d104]
| | | | Frame[function=$mpi__main, location=257, wave1dBad.c:265.6-14 "exchange", dyscope=d48]
| | | | Frame[function=MPI_Process, location=146, MPItoCIVLTransformer:0.-1 "" inserted by MPItoCIVLTransformer.function call $mpi__mainbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from civlc.cvl:9.9-20 "<civlc.cvh>", dyscope=d8]

Logging new entry 0, writing trace to CIVLREP/wave1dBad_0.trace

Error bound exceeded: search terminated

=================== Stats ===================
   validCalls          : 7282
   proverCalls         : 48
   memory (bytes)      : 650117120
   time (s)            : 3.86
   maxProcs            : 3
   statesInstantiated  : 12562
   statesSaved         : 1324
   statesSeen          : 1247
   statesMatched       : 0
   steps               : 2018
   transitions         : 1246

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.02 s (62.9 files/s, 26555.8 lines/s)"
1,C,34,93,295
civl verify -enablePrintf=false  gausselim.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
18s: mem=892Mb steps=35420 trans=21705 seen=21706 saved=22529 prove=560
33s: mem=1221Mb steps=72032 trans=44209 seen=44209 saved=45844 prove=1132
48s: mem=1113Mb steps=124010 trans=76278 seen=76279 saved=79084 prove=1606
63s: mem=936Mb steps=169218 trans=103804 seen=103804 saved=107753 prove=1928
78s: mem=790Mb steps=215591 trans=132194 seen=132195 saved=137296 prove=2231
93s: mem=699Mb steps=246766 trans=151177 seen=151178 saved=157063 prove=2705
108s: mem=533Mb steps=312140 trans=191345 seen=191346 saved=198803 prove=2777

=================== Stats ===================
   validCalls          : 1442028
   proverCalls         : 2777
   memory (bytes)      : 552599552
   time (s)            : 107.69
   maxProcs            : 4
   statesInstantiated  : 2026847
   statesSaved         : 200306
   statesSeen          : 192791
   statesMatched       : 0
   steps               : 314435
   transitions         : 192790

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.02 s (63.9 files/s, 8242.8 lines/s)"
1,C,11,13,105
civl verify -enablePrintf=false  matmat_mw/matmat_mw.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
17s: mem=1298Mb steps=37726 trans=22199 seen=22179 saved=23131 prove=350
32s: mem=1045Mb steps=64370 trans=37735 seen=37691 saved=39315 prove=478

=================== Stats ===================
   validCalls          : 600035
   proverCalls         : 518
   memory (bytes)      : 847249408
   time (s)            : 42.76
   maxProcs            : 5
   statesInstantiated  : 534488
   statesSaved         : 49343
   statesSeen          : 47307
   statesMatched       : 90
   steps               : 80548
   transitions         : 47396

The standard properties hold for all executions.
