NAME: diffusion1d.c
CITE: 
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 (114.7 files/s, 24202.8 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=1327Mb steps=41841 trans=25234 seen=25235 saved=26094 prove=274
32s: mem=1104Mb steps=94107 trans=56396 seen=56396 saved=58511 prove=379

=================== Stats ===================
   validCalls          : 452505
   proverCalls         : 399
   memory (bytes)      : 1060634624
   time (s)            : 37.56
   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: 
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, 23260.3 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=1327Mb steps=35040 trans=23064 seen=23064 saved=23974 prove=115
33s: mem=1104Mb steps=69892 trans=45603 seen=45604 saved=47449 prove=166
48s: mem=932Mb steps=103859 trans=67172 seen=67173 saved=69868 prove=221
63s: mem=773Mb steps=131153 trans=84168 seen=84169 saved=87593 prove=257
78s: mem=611Mb steps=157627 trans=100819 seen=100820 saved=104950 prove=281
93s: mem=487Mb steps=180955 trans=115207 seen=115208 saved=119922 prove=293
108s: mem=477Mb steps=212740 trans=135407 seen=135407 saved=140894 prove=348
123s: mem=513Mb steps=237276 trans=150741 seen=150741 saved=156868 prove=384
138s: mem=474Mb steps=261087 trans=165597 seen=165598 saved=172319 prove=400
153s: mem=503Mb steps=284341 trans=180321 seen=180322 saved=187667 prove=420
168s: mem=503Mb steps=310081 trans=196767 seen=196768 saved=204714 prove=470
183s: mem=579Mb steps=336307 trans=213162 seen=213163 saved=221770 prove=502
198s: mem=596Mb steps=358575 trans=227009 seen=227010 saved=236165 prove=522
213s: mem=527Mb steps=375116 trans=237325 seen=237326 saved=246893 prove=534
228s: mem=620Mb steps=396558 trans=250847 seen=250848 saved=260950 prove=550
243s: mem=557Mb steps=417259 trans=264056 seen=264056 saved=274616 prove=583
258s: mem=530Mb steps=442838 trans=280188 seen=280189 saved=291376 prove=615
273s: mem=634Mb steps=460352 trans=290923 seen=290924 saved=302521 prove=623
288s: mem=622Mb steps=482099 trans=304743 seen=304744 saved=316884 prove=651
303s: mem=828Mb steps=499214 trans=315473 seen=315473 saved=328039 prove=663
318s: mem=827Mb steps=514018 trans=324655 seen=324656 saved=337562 prove=671

=================== Stats ===================
   validCalls          : 2597686
   proverCalls         : 671
   memory (bytes)      : 813694976
   time (s)            : 325.02
   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: 
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 (131.5 files/s, 18012.6 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=624Mb steps=18891 trans=9624 seen=9625 saved=10006 prove=705

=================== Stats ===================
   validCalls          : 64634
   proverCalls         : 766
   memory (bytes)      : 654311424
   time (s)            : 18.72
   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: 
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 (65.2 files/s, 10950.3 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=601Mb steps=14843 trans=8501 seen=8502 saved=8786 prove=687
32s: mem=539Mb steps=27552 trans=15728 seen=15729 saved=16233 prove=1343
47s: mem=485Mb steps=40643 trans=23194 seen=23195 saved=23926 prove=2020
62s: mem=442Mb steps=54108 trans=30870 seen=30871 saved=31835 prove=2703
77s: mem=408Mb steps=66847 trans=38147 seen=38148 saved=39334 prove=3367
92s: mem=399Mb steps=79269 trans=45235 seen=45236 saved=46638 prove=4014
107s: mem=400Mb steps=92014 trans=52511 seen=52512 saved=54137 prove=4681
122s: mem=394Mb steps=104852 trans=59852 seen=59853 saved=61701 prove=5343

=================== Stats ===================
   validCalls          : 367307
   proverCalls         : 5798
   memory (bytes)      : 425197568
   time (s)            : 132.47
   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: 
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.01 s (71.2 files/s, 6119.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=849Mb steps=40633 trans=25079 seen=24920 saved=26190 prove=337

=================== Stats ===================
   validCalls          : 492299
   proverCalls         : 409
   memory (bytes)      : 1324351488
   time (s)            : 23.9
   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: 
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 (65.0 files/s, 17671.7 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=45482 trans=27562 seen=27563 saved=29055 prove=219
33s: mem=1099Mb steps=86779 trans=52678 seen=52678 saved=55596 prove=315

=================== Stats ===================
   validCalls          : 434780
   proverCalls         : 335
   memory (bytes)      : 1085800448
   time (s)            : 37.68
   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: 
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 (64.2 files/s, 17716.2 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(2,(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.97
   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: 
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 (59.8 files/s, 25255.7 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=33639 trans=20615 seen=20616 saved=21402 prove=550
33s: mem=1276Mb steps=68677 trans=42167 seen=42168 saved=43728 prove=1091
48s: mem=1112Mb steps=117134 trans=72081 seen=72082 saved=74707 prove=1606
63s: mem=960Mb steps=162202 trans=99528 seen=99529 saved=103305 prove=1883
78s: mem=827Mb steps=209213 trans=128340 seen=128341 saved=133279 prove=2151
93s: mem=712Mb steps=242052 trans=148278 seen=148279 saved=154041 prove=2592
108s: mem=563Mb steps=297440 trans=182233 seen=182234 saved=189346 prove=2743

=================== Stats ===================
   validCalls          : 1442028
   proverCalls         : 2777
   memory (bytes)      : 552599552
   time (s)            : 111.39
   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: 
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.01 s (71.1 files/s, 9165.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=1295Mb steps=37065 trans=21817 seen=21799 saved=22733 prove=342
32s: mem=1040Mb steps=63530 trans=37247 seen=37204 saved=38804 prove=470

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

The standard properties hold for all executions.
