/opt/local/bin/civl-1.7.1 compare -checkMemoryLeak=false -spec treebuffer-driver.cvl treebuffer-naive.c -impl treebuffer-driver.cvl treebuffer-realtime.c
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
17s: mem=31403Mb trans=211418 traceSteps=151954 explored=211420 saved=200442 prove=127
32s: mem=31403Mb trans=501885 traceSteps=360943 explored=501886 saved=475890 prove=226
47s: mem=31403Mb trans=786353 traceSteps=565893 explored=786354 saved=746134 prove=340
63s: mem=32050Mb trans=1067369 traceSteps=768665 explored=1067368 saved=1013301 prove=439
78s: mem=31956Mb trans=1346347 traceSteps=969742 explored=1346348 saved=1277410 prove=538
93s: mem=32160Mb trans=1631329 traceSteps=1174885 explored=1631330 saved=1547903 prove=637
108s: mem=32189Mb trans=1909517 traceSteps=1375348 explored=1909518 saved=1812371 prove=736
123s: mem=31702Mb trans=2194905 traceSteps=1581174 explored=2194906 saved=2084084 prove=823
138s: mem=32161Mb trans=2473605 traceSteps=1782330 explored=2473606 saved=2348569 prove=922
153s: mem=32167Mb trans=2748809 traceSteps=1980754 explored=2748810 saved=2609898 prove=1021
168s: mem=32167Mb trans=3020807 traceSteps=2176994 explored=3020808 saved=2868641 prove=1120
183s: mem=32193Mb trans=3294736 traceSteps=2374773 explored=3294737 saved=3129566 prove=1207
198s: mem=32181Mb trans=3550537 traceSteps=2559680 explored=3550538 saved=3373607 prove=1321
213s: mem=32233Mb trans=3818328 traceSteps=2753145 explored=3818329 saved=3627482 prove=1420
228s: mem=32268Mb trans=4087475 traceSteps=2947088 explored=4087476 saved=3881660 prove=1507
243s: mem=32251Mb trans=4352886 traceSteps=3138629 explored=4352887 saved=4132845 prove=1597
258s: mem=32304Mb trans=4616562 traceSteps=3328929 explored=4616562 saved=4382574 prove=1693
273s: mem=32285Mb trans=4873679 traceSteps=3514783 explored=4873680 saved=4626153 prove=1780
288s: mem=32341Mb trans=5130565 traceSteps=3700251 explored=5130566 saved=4868773 prove=1888
303s: mem=32321Mb trans=5402697 traceSteps=3896016 explored=5402698 saved=5126853 prove=1975
318s: mem=32359Mb trans=5661536 traceSteps=4082438 explored=5661537 saved=5372697 prove=2062
333s: mem=32409Mb trans=5915572 traceSteps=4265779 explored=5915572 saved=5614512 prove=2156
348s: mem=32392Mb trans=6170925 traceSteps=4450061 explored=6170924 saved=5857193 prove=2248
363s: mem=32441Mb trans=6419602 traceSteps=4629426 explored=6419603 saved=6092916 prove=2335
378s: mem=32425Mb trans=6668024 traceSteps=4808509 explored=6668025 saved=6329050 prove=2422
393s: mem=32418Mb trans=6922568 traceSteps=4992230 explored=6922569 saved=6571372 prove=2509
408s: mem=32437Mb trans=7169247 traceSteps=5170357 explored=7169247 saved=6806481 prove=2596
423s: mem=32463Mb trans=7416439 traceSteps=5349046 explored=7416440 saved=7041931 prove=2683
438s: mem=32450Mb trans=7657274 traceSteps=5522975 explored=7657274 saved=7270502 prove=2782
453s: mem=32488Mb trans=7909868 traceSteps=5705084 explored=7909869 saved=7510719 prove=2869
468s: mem=32475Mb trans=8148892 traceSteps=5877717 explored=8148892 saved=7738507 prove=2956
483s: mem=32510Mb trans=8384916 traceSteps=6048367 explored=8384917 saved=7963774 prove=3031
498s: mem=32499Mb trans=8624056 traceSteps=6221288 explored=8624056 saved=8192004 prove=3118
513s: mem=32531Mb trans=8866759 traceSteps=6396739 explored=8866760 saved=8422358 prove=3217
528s: mem=32549Mb trans=9116387 traceSteps=6576635 explored=9116388 saved=8658238 prove=3304
543s: mem=32541Mb trans=9357205 traceSteps=6750500 explored=9357206 saved=8886321 prove=3391
558s: mem=32566Mb trans=9598661 traceSteps=6925004 explored=9598661 saved=9115363 prove=3451
573s: mem=32558Mb trans=9829651 traceSteps=7091973 explored=9829652 saved=9334663 prove=3538
588s: mem=32580Mb trans=10064799 traceSteps=7261990 explored=10064800 saved=9556840 prove=3613
603s: mem=32573Mb trans=10295496 traceSteps=7428021 explored=10295497 saved=9774172 prove=3721
618s: mem=32592Mb trans=10535611 traceSteps=7600764 explored=10535612 saved=10000499 prove=3796
633s: mem=32586Mb trans=10766661 traceSteps=7767264 explored=10766662 saved=10218721 prove=3883
648s: mem=32586Mb trans=10999238 traceSteps=7935105 explored=10999239 saved=10438762 prove=3958
663s: mem=32602Mb trans=11229058 traceSteps=8100964 explored=11229059 saved=10655718 prove=4045
678s: mem=32597Mb trans=11465226 traceSteps=8271298 explored=11465227 saved=10878293 prove=4132
693s: mem=32610Mb trans=11699668 traceSteps=8440322 explored=11699669 saved=11099827 prove=4219
708s: mem=32607Mb trans=11917236 traceSteps=8597362 explored=11917237 saved=11305697 prove=4294
723s: mem=32618Mb trans=12146509 traceSteps=8762886 explored=12146510 saved=11522905 prove=4354
738s: mem=32615Mb trans=12363160 traceSteps=8919471 explored=12363161 saved=11728514 prove=4441
753s: mem=32623Mb trans=12583720 traceSteps=9078816 explored=12583721 saved=11936615 prove=4516
768s: mem=32621Mb trans=12790030 traceSteps=9227589 explored=12790030 saved=12131338 prove=4603
783s: mem=32628Mb trans=13019068 traceSteps=9392713 explored=13019069 saved=12347875 prove=4678
798s: mem=32626Mb trans=13243363 traceSteps=9554738 explored=13243363 saved=12560410 prove=4753
813s: mem=32632Mb trans=13438760 traceSteps=9696049 explored=13438761 saved=12745849 prove=4828
828s: mem=32630Mb trans=13653653 traceSteps=9851452 explored=13653654 saved=12949955 prove=4888
843s: mem=32636Mb trans=13880923 traceSteps=10015766 explored=13880924 saved=13164655 prove=4963
858s: mem=32627Mb trans=14095187 traceSteps=10170176 explored=14095187 saved=13365968 prove=5062
873s: mem=32635Mb trans=14326337 traceSteps=10336788 explored=14326338 saved=13583206 prove=5137
888s: mem=32635Mb trans=14544416 traceSteps=10494337 explored=14544417 saved=13788670 prove=5212
903s: mem=32633Mb trans=14764524 traceSteps=10653417 explored=14764525 saved=13996290 prove=5287
918s: mem=32638Mb trans=14982418 traceSteps=10810979 explored=14982419 saved=14201805 prove=5362
933s: mem=32637Mb trans=15203185 traceSteps=10970691 explored=15203186 saved=14409141 prove=5437
948s: mem=32636Mb trans=15418180 traceSteps=11125010 explored=15418181 saved=14611508 prove=5536
963s: mem=32632Mb trans=15639196 traceSteps=11283670 explored=15639196 saved=14819442 prove=5611
978s: mem=32637Mb trans=15842597 traceSteps=11429880 explored=15842597 saved=15011066 prove=5674
993s: mem=32636Mb trans=16052398 traceSteps=11581045 explored=16052399 saved=15209190 prove=5749
1008s: mem=32639Mb trans=16258399 traceSteps=11729694 explored=16258400 saved=15403868 prove=5824
1023s: mem=32638Mb trans=16473717 traceSteps=11884879 explored=16473716 saved=15606278 prove=5884
1038s: mem=32638Mb trans=16689084 traceSteps=12039542 explored=16689085 saved=15809051 prove=5971
1053s: mem=32640Mb trans=16903876 traceSteps=12193920 explored=16903877 saved=16011390 prove=6046
1068s: mem=32640Mb trans=17114801 traceSteps=12345687 explored=17114802 saved=16210361 prove=6121
1083s: mem=32641Mb trans=17328594 traceSteps=12499711 explored=17328595 saved=16412358 prove=6196
1098s: mem=32640Mb trans=17501773 traceSteps=12624846 explored=17501774 saved=16576454 prove=6271
1113s: mem=32643Mb trans=17714096 traceSteps=12777813 explored=17714096 saved=16776177 prove=6320
1128s: mem=32642Mb trans=17908771 traceSteps=12917922 explored=17908771 saved=16959558 prove=6406
1143s: mem=32642Mb trans=18114601 traceSteps=13066357 explored=18114601 saved=17154027 prove=6481
1158s: mem=32644Mb trans=18312409 traceSteps=13209150 explored=18312410 saved=17341187 prove=6556
1173s: mem=32644Mb trans=18491566 traceSteps=13338502 explored=18491567 saved=17510926 prove=6604
1188s: mem=32646Mb trans=18688576 traceSteps=13480838 explored=18688577 saved=17697647 prove=6679
1203s: mem=32645Mb trans=18883000 traceSteps=13621305 explored=18883000 saved=17881285 prove=6742
1218s: mem=32645Mb trans=19066442 traceSteps=13753842 explored=19066442 saved=18054118 prove=6817
1233s: mem=32643Mb trans=19281863 traceSteps=13908911 explored=19281864 saved=18256202 prove=6877
1248s: mem=32644Mb trans=19490093 traceSteps=14058835 explored=19490094 saved=18451869 prove=6952
1263s: mem=32645Mb trans=19690318 traceSteps=14203015 explored=19690318 saved=18639885 prove=7027
1278s: mem=32644Mb trans=19882645 traceSteps=14341847 explored=19882646 saved=18820947 prove=7102
1293s: mem=32646Mb trans=20077394 traceSteps=14482617 explored=20077395 saved=19004465 prove=7165
1308s: mem=32646Mb trans=20289919 traceSteps=14636030 explored=20289919 saved=19203628 prove=7225
1323s: mem=32646Mb trans=20482195 traceSteps=14774335 explored=20482196 saved=19384749 prove=7321
1338s: mem=32648Mb trans=20689885 traceSteps=14923671 explored=20689886 saved=19580515 prove=7384
1353s: mem=32647Mb trans=20874075 traceSteps=15056365 explored=20874076 saved=19754433 prove=7459
1368s: mem=32648Mb trans=21055332 traceSteps=15187189 explored=21055332 saved=19925996 prove=7507
1383s: mem=32648Mb trans=21245446 traceSteps=15324352 explored=21245447 saved=20105919 prove=7570
1398s: mem=32648Mb trans=21441689 traceSteps=15465910 explored=21441690 saved=20291010 prove=7645
1413s: mem=32649Mb trans=21629937 traceSteps=15601820 explored=21629937 saved=20468429 prove=7729
1428s: mem=32649Mb trans=21815540 traceSteps=15735540 explored=21815541 saved=20643745 prove=7780
1443s: mem=32557Mb trans=21997095 traceSteps=15866419 explored=21997095 saved=20815287 prove=7843
1458s: mem=32603Mb trans=22181454 traceSteps=15999518 explored=22181454 saved=20989701 prove=7913
1473s: mem=32603Mb trans=22349360 traceSteps=16120836 explored=22349360 saved=21148786 prove=7954
1488s: mem=32609Mb trans=22514060 traceSteps=16239767 explored=22514061 saved=21304916 prove=8017
1503s: mem=32607Mb trans=22693175 traceSteps=16369215 explored=22693175 saved=21474188 prove=8092
1518s: mem=32612Mb trans=22867184 traceSteps=16495056 explored=22867185 saved=21638405 prove=8167
1533s: mem=32612Mb trans=23054603 traceSteps=16630043 explored=23054603 saved=21815561 prove=8215
1548s: mem=32610Mb trans=23241375 traceSteps=16764709 explored=23241375 saved=21992130 prove=8290
1563s: mem=32615Mb trans=23424879 traceSteps=16897243 explored=23424879 saved=22165953 prove=8353
1578s: mem=32614Mb trans=23609411 traceSteps=17030740 explored=23609412 saved=22341113 prove=8401
1593s: mem=32614Mb trans=23780753 traceSteps=17154565 explored=23780754 saved=22503744 prove=8464
1608s: mem=32620Mb trans=23951891 traceSteps=17278249 explored=23951892 saved=22665629 prove=8527
1623s: mem=32617Mb trans=24122344 traceSteps=17401610 explored=24122344 saved=22826693 prove=8611
1638s: mem=32624Mb trans=24319300 traceSteps=17543383 explored=24319300 saved=23011655 prove=8662
1653s: mem=32624Mb trans=24507543 traceSteps=17679128 explored=24507543 saved=23188618 prove=8733
1668s: mem=32622Mb trans=24678138 traceSteps=17802365 explored=24678138 saved=23349316 prove=8795
1683s: mem=32622Mb trans=24847696 traceSteps=17924964 explored=24847697 saved=23509390 prove=8836
1698s: mem=32624Mb trans=25020879 traceSteps=18050055 explored=25020879 saved=23672574 prove=8911
1713s: mem=32624Mb trans=25190977 traceSteps=18173034 explored=25190977 saved=23832850 prove=8974
1728s: mem=32628Mb trans=25392023 traceSteps=18318444 explored=25392023 saved=24021672 prove=9022
1743s: mem=32626Mb trans=25574327 traceSteps=18449297 explored=25574328 saved=24192262 prove=9118
1758s: mem=32632Mb trans=25763636 traceSteps=18585239 explored=25763636 saved=24369408 prove=9181
1773s: mem=32632Mb trans=25928524 traceSteps=18703848 explored=25928524 saved=24524028 prove=9244
1788s: mem=32630Mb trans=26123841 traceSteps=18844532 explored=26123841 saved=24707576 prove=9292
1803s: mem=32635Mb trans=26299099 traceSteps=18970873 explored=26299100 saved=24872221 prove=9355
1818s: mem=32634Mb trans=26481789 traceSteps=19102698 explored=26481789 saved=25043844 prove=9430
1833s: mem=32634Mb trans=26627864 traceSteps=19207960 explored=26627865 saved=25180543 prove=9466
1848s: mem=32638Mb trans=26793255 traceSteps=19326916 explored=26793255 saved=25335287 prove=9541
1863s: mem=32637Mb trans=26988858 traceSteps=19467794 explored=26988858 saved=25518871 prove=9604
1878s: mem=32640Mb trans=27164009 traceSteps=19594026 explored=27164010 saved=25683570 prove=9664
1893s: mem=32640Mb trans=27346094 traceSteps=19725108 explored=27346095 saved=25854514 prove=9727
1908s: mem=32639Mb trans=27508294 traceSteps=19842165 explored=27508295 saved=26007181 prove=9790
1923s: mem=32550Mb trans=27673635 traceSteps=19961733 explored=27673636 saved=26163278 prove=9838
1938s: mem=32596Mb trans=27847877 traceSteps=20087429 explored=27847878 saved=26326518 prove=9901
1953s: mem=32596Mb trans=27990533 traceSteps=20190433 explored=27990533 saved=26460279 prove=9964
1968s: mem=32600Mb trans=28160002 traceSteps=20312464 explored=28160005 saved=26619519 prove=10012
1983s: mem=32597Mb trans=28327726 traceSteps=20433387 explored=28327726 saved=26777119 prove=10075
1998s: mem=32597Mb trans=28477243 traceSteps=20541433 explored=28477243 saved=26918009 prove=10111
2013s: mem=32604Mb trans=28627027 traceSteps=20649580 explored=28627027 saved=27059109 prove=10174
2028s: mem=32602Mb trans=28768121 traceSteps=20751604 explored=28768123 saved=27192183 prove=10225
2043s: mem=32602Mb trans=28917411 traceSteps=20859521 explored=28917411 saved=27333159 prove=10273
2058s: mem=32609Mb trans=29080346 traceSteps=20977261 explored=29080346 saved=27486351 prove=10336
2073s: mem=32606Mb trans=29243288 traceSteps=21095141 explored=29243288 saved=27639407 prove=10372
2088s: mem=32606Mb trans=29431828 traceSteps=21230706 explored=29431828 saved=27815336 prove=10459
2103s: mem=32615Mb trans=29606147 traceSteps=21356185 explored=29606146 saved=27978041 prove=10522
2118s: mem=32612Mb trans=29768826 traceSteps=21473590 explored=29768826 saved=28130330 prove=10562
2133s: mem=32612Mb trans=29923288 traceSteps=21584867 explored=29923288 saved=28274852 prove=10621
2148s: mem=32620Mb trans=30090366 traceSteps=21705542 explored=30090366 saved=28431426 prove=10684
2163s: mem=32618Mb trans=30247916 traceSteps=21819528 explored=30247917 saved=28579509 prove=10732
2178s: mem=32625Mb trans=30424929 traceSteps=21947189 explored=30424929 saved=28744531 prove=10795

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


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

=== Stats ===
   time (s)            : 2189.78
   memory (bytes)      : 34210316288
   max process count   : 1
   states              : 30543383
   states saved        : 28855134
   state matches       : 0
   transitions         : 30543382
   trace steps         : 22032865
   valid calls         : 58436744
   provers             : z3
   prover calls        : 10819

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