/opt/local/bin/civl-1.7.1 compare -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-caterpillar.c
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
17s: mem=31403Mb trans=235611 traceSteps=161846 explored=235611 saved=221210 prove=209
32s: mem=31403Mb trans=556178 traceSteps=383444 explored=556178 saved=524150 prove=400
47s: mem=31403Mb trans=858189 traceSteps=591772 explored=858190 saved=809377 prove=625
62s: mem=31403Mb trans=1170784 traceSteps=808026 explored=1170784 saved=1105113 prove=811
77s: mem=31930Mb trans=1473344 traceSteps=1017738 explored=1473344 saved=1392215 prove=1021
92s: mem=31837Mb trans=1766820 traceSteps=1221136 explored=1766820 saved=1670156 prove=1203
107s: mem=32039Mb trans=2056107 traceSteps=1422577 explored=2056108 saved=1945951 prove=1408
122s: mem=32080Mb trans=2348604 traceSteps=1624642 explored=2348607 saved=2222856 prove=1606
137s: mem=31509Mb trans=2638775 traceSteps=1826332 explored=2638775 saved=2499746 prove=1792
152s: mem=32059Mb trans=2918373 traceSteps=2019516 explored=2918374 saved=2764145 prove=1987
167s: mem=32063Mb trans=3198673 traceSteps=2213580 explored=3198674 saved=3029161 prove=2161
182s: mem=32084Mb trans=3470392 traceSteps=2401928 explored=3470392 saved=3286832 prove=2357
197s: mem=32065Mb trans=3745846 traceSteps=2592614 explored=3745847 saved=3547338 prove=2533
212s: mem=32106Mb trans=4018159 traceSteps=2782069 explored=4018160 saved=3806453 prove=2707
227s: mem=32093Mb trans=4287906 traceSteps=2969210 explored=4287907 saved=4062109 prove=2893
242s: mem=32140Mb trans=4555320 traceSteps=3155418 explored=4555321 saved=4316367 prove=3055
257s: mem=32122Mb trans=4821173 traceSteps=3340603 explored=4821174 saved=4569760 prove=3253
272s: mem=32182Mb trans=5093797 traceSteps=3529834 explored=5093798 saved=4829043 prove=3427
287s: mem=32161Mb trans=5357177 traceSteps=3713602 explored=5357177 saved=5081246 prove=3601
302s: mem=32228Mb trans=5622325 traceSteps=3896683 explored=5622325 saved=5331941 prove=3796
317s: mem=32204Mb trans=5874365 traceSteps=4071141 explored=5874368 saved=5570724 prove=3958
332s: mem=32204Mb trans=6132435 traceSteps=4249966 explored=6132435 saved=5816105 prove=4144
347s: mem=32273Mb trans=6384992 traceSteps=4424704 explored=6384993 saved=6055625 prove=4318
362s: mem=32250Mb trans=6629394 traceSteps=4594704 explored=6629394 saved=6289005 prove=4480
377s: mem=32294Mb trans=6867484 traceSteps=4759990 explored=6867484 saved=6516038 prove=4654
392s: mem=32294Mb trans=7122084 traceSteps=4936910 explored=7122084 saved=6758386 prove=4801
407s: mem=32332Mb trans=7358821 traceSteps=5102093 explored=7358821 saved=6985141 prove=4963
422s: mem=32313Mb trans=7607670 traceSteps=5274572 explored=7607670 saved=7222174 prove=5149
437s: mem=32313Mb trans=7847029 traceSteps=5441183 explored=7847029 saved=7451585 prove=5311
452s: mem=32371Mb trans=8076792 traceSteps=5600937 explored=8076793 saved=7671875 prove=5500
467s: mem=32352Mb trans=8319944 traceSteps=5768193 explored=8319944 saved=7900918 prove=5662
482s: mem=32404Mb trans=8561377 traceSteps=5935143 explored=8561377 saved=8129538 prove=5797
497s: mem=32389Mb trans=8801349 traceSteps=6100655 explored=8801349 saved=8356551 prove=5971
512s: mem=32389Mb trans=9040874 traceSteps=6265939 explored=9040874 saved=8582715 prove=6133
527s: mem=32434Mb trans=9271876 traceSteps=6426150 explored=9271877 saved=8802112 prove=6295
542s: mem=32420Mb trans=9503703 traceSteps=6586538 explored=9503703 saved=9022040 prove=6457
557s: mem=32462Mb trans=9717161 traceSteps=6734389 explored=9717161 saved=9224405 prove=6592
572s: mem=32462Mb trans=9940327 traceSteps=6889594 explored=9940327 saved=9437167 prove=6742
587s: mem=32449Mb trans=10165517 traceSteps=7045494 explored=10165517 saved=9651398 prove=6914
602s: mem=32489Mb trans=10401504 traceSteps=7209113 explored=10401504 saved=9876404 prove=7056
617s: mem=32476Mb trans=10613142 traceSteps=7356231 explored=10613143 saved=10079051 prove=7213
632s: mem=32476Mb trans=10833021 traceSteps=7507878 explored=10833021 saved=10287223 prove=7372
647s: mem=32510Mb trans=11041510 traceSteps=7652069 explored=11041510 saved=10484788 prove=7507
662s: mem=32500Mb trans=11257823 traceSteps=7802049 explored=11257823 saved=10690632 prove=7657
677s: mem=32500Mb trans=11474830 traceSteps=7952131 explored=11474830 saved=10896464 prove=7819
692s: mem=32527Mb trans=11672078 traceSteps=8088774 explored=11672081 saved=11083498 prove=7930
707s: mem=32519Mb trans=11863687 traceSteps=8222092 explored=11863687 saved=11266144 prove=8068
722s: mem=32519Mb trans=12064446 traceSteps=8361424 explored=12064446 saved=11457410 prove=8203
737s: mem=32544Mb trans=12278150 traceSteps=8509706 explored=12278150 saved=11660658 prove=8353
752s: mem=32536Mb trans=12470294 traceSteps=8643683 explored=12470295 saved=11844156 prove=8476
767s: mem=32536Mb trans=12676041 traceSteps=8787019 explored=12676041 saved=12041254 prove=8638
782s: mem=32559Mb trans=12891460 traceSteps=8936456 explored=12891460 saved=12246868 prove=8788
797s: mem=32552Mb trans=13087819 traceSteps=9073076 explored=13087820 saved=12434760 prove=8911
812s: mem=32552Mb trans=13261812 traceSteps=9194663 explored=13261812 saved=12602715 prove=9022
827s: mem=32570Mb trans=13465515 traceSteps=9334812 explored=13465516 saved=12795188 prove=9193
842s: mem=32565Mb trans=13658609 traceSteps=9468410 explored=13658609 saved=12978710 prove=9328
857s: mem=32565Mb trans=13872970 traceSteps=9616971 explored=13872970 saved=13183170 prove=9466
872s: mem=32578Mb trans=14083381 traceSteps=9762292 explored=14083381 saved=13383148 prove=9616
887s: mem=32576Mb trans=14270925 traceSteps=9892258 explored=14270926 saved=13561656 prove=9739
902s: mem=32576Mb trans=14452718 traceSteps=10018683 explored=14452718 saved=13735695 prove=9877
917s: mem=32586Mb trans=14652401 traceSteps=10157223 explored=14652401 saved=13926687 prove=10012
932s: mem=32586Mb trans=14853390 traceSteps=10296681 explored=14853390 saved=14118473 prove=10152
947s: mem=32583Mb trans=15023806 traceSteps=10415474 explored=15023807 saved=14281894 prove=10273
962s: mem=32583Mb trans=15209604 traceSteps=10545064 explored=15209605 saved=14460975 prove=10419
977s: mem=32591Mb trans=15399142 traceSteps=10676254 explored=15399143 saved=14641962 prove=10546
992s: mem=32590Mb trans=15583681 traceSteps=10804640 explored=15583681 saved=14819459 prove=10682
1007s: mem=32590Mb trans=15774518 traceSteps=10937781 explored=15774519 saved=15003919 prove=10807

=== Source files ===
treebuffer-driver.cvl  (treebuffer-driver.cvl)
treebuffer.h  (treebuffer.h)
treebuffer-naive.c  (treebuffer-naive.c)
treebuffer-caterpillar.c  (treebuffer-caterpillar.c)


=== Command ===
civl compare -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-caterpillar.c 

=== Stats ===
   time (s)            : 1009.21
   memory (bytes)      : 34173616128
   max process count   : 1
   states              : 15805485
   states saved        : 15034296
   state matches       : 0
   transitions         : 15805484
   trace steps         : 10959547
   valid calls         : 25767724
   provers             : z3
   prover calls        : 10819

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