/opt/local/bin/civl-1.7.1 verify treebuffer-driver.cvl treebuffer-realtime.c 
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
17s: mem=31403Mb trans=90380 traceSteps=66272 explored=90380 saved=88752 prove=404
32s: mem=31403Mb trans=203403 traceSteps=149019 explored=203404 saved=199710 prove=805
47s: mem=31403Mb trans=325947 traceSteps=238479 explored=325947 saved=319198 prove=1226
62s: mem=31403Mb trans=440302 traceSteps=321999 explored=440302 saved=430813 prove=1651
77s: mem=31403Mb trans=557411 traceSteps=407619 explored=557413 saved=545531 prove=2074
92s: mem=31403Mb trans=673675 traceSteps=492326 explored=673675 saved=658887 prove=2505
107s: mem=31403Mb trans=792821 traceSteps=579027 explored=792821 saved=774140 prove=2912
122s: mem=31976Mb trans=912407 traceSteps=666120 explored=912407 saved=889809 prove=3309
137s: mem=31976Mb trans=1032193 traceSteps=753125 explored=1032194 saved=1005339 prove=3712
152s: mem=31910Mb trans=1151034 traceSteps=839467 explored=1151035 saved=1119617 prove=4088
167s: mem=32076Mb trans=1265514 traceSteps=923408 explored=1265515 saved=1232372 prove=4438
182s: mem=32076Mb trans=1382513 traceSteps=1009078 explored=1382514 saved=1347562 prove=4787
197s: mem=32063Mb trans=1502899 traceSteps=1096842 explored=1502899 saved=1464398 prove=5116
212s: mem=32108Mb trans=1602328 traceSteps=1169827 explored=1602328 saved=1562530 prove=5491
227s: mem=32108Mb trans=1725979 traceSteps=1261090 explored=1725978 saved=1685056 prove=5802
242s: mem=31575Mb trans=1873556 traceSteps=1369690 explored=1873556 saved=1829897 prove=6052
257s: mem=32098Mb trans=2013161 traceSteps=1472576 explored=2013161 saved=1967854 prove=6326
272s: mem=32100Mb trans=2178685 traceSteps=1594183 explored=2178685 saved=2130187 prove=6548
287s: mem=32108Mb trans=2329089 traceSteps=1704959 explored=2329089 saved=2278206 prove=6794
302s: mem=32102Mb trans=2495690 traceSteps=1827456 explored=2495690 saved=2441741 prove=7016
317s: mem=32135Mb trans=2654061 traceSteps=1943535 explored=2654062 saved=2595466 prove=7244
332s: mem=32135Mb trans=2827701 traceSteps=2070608 explored=2827701 saved=2763669 prove=7446
347s: mem=32119Mb trans=2966628 traceSteps=2172105 explored=2966628 saved=2898370 prove=7727
362s: mem=32173Mb trans=3100158 traceSteps=2270257 explored=3100158 saved=3029964 prove=8016
377s: mem=32153Mb trans=3265982 traceSteps=2392418 explored=3265982 saved=3193154 prove=8224
392s: mem=32224Mb trans=3404972 traceSteps=2494254 explored=3404972 saved=3329122 prove=8504
407s: mem=32224Mb trans=3540516 traceSteps=2594054 explored=3540516 saved=3462776 prove=8779
422s: mem=32192Mb trans=3703618 traceSteps=2714056 explored=3703619 saved=3623069 prove=8983
437s: mem=32262Mb trans=3857513 traceSteps=2826942 explored=3857513 saved=3773600 prove=9220
452s: mem=32243Mb trans=4007816 traceSteps=2937480 explored=4007819 saved=3921658 prove=9453
467s: mem=32305Mb trans=4178635 traceSteps=3062392 explored=4178635 saved=4088068 prove=9661
482s: mem=32305Mb trans=4345268 traceSteps=3184272 explored=4345269 saved=4249529 prove=9883
497s: mem=32286Mb trans=4505746 traceSteps=3301524 explored=4505747 saved=4404913 prove=10101
512s: mem=32346Mb trans=4676322 traceSteps=3425671 explored=4676322 saved=4568552 prove=10307
527s: mem=32326Mb trans=4840250 traceSteps=3545724 explored=4840250 saved=4727437 prove=10523
542s: mem=32386Mb trans=5015561 traceSteps=3674145 explored=5015561 saved=4897096 prove=10707
557s: mem=32367Mb trans=5160287 traceSteps=3779659 explored=5160288 saved=5036471 prove=10960
572s: mem=32367Mb trans=5293666 traceSteps=3877278 explored=5293666 saved=5165936 prove=11229
587s: mem=32422Mb trans=5455638 traceSteps=3995891 explored=5455639 saved=5322943 prove=11420
602s: mem=32406Mb trans=5615676 traceSteps=4112645 explored=5615677 saved=5476951 prove=11627
617s: mem=32452Mb trans=5777548 traceSteps=4231029 explored=5777549 saved=5633720 prove=11834
632s: mem=32452Mb trans=5949873 traceSteps=4356710 explored=5949873 saved=5799839 prove=12019
647s: mem=32437Mb trans=6132590 traceSteps=4489644 explored=6132591 saved=5974154 prove=12186
662s: mem=32481Mb trans=6297720 traceSteps=4609794 explored=6297720 saved=6131817 prove=12384
677s: mem=32466Mb trans=6476773 traceSteps=4739612 explored=6476773 saved=6301619 prove=12538
692s: mem=32431Mb trans=6591789 traceSteps=4823247 explored=6591789 saved=6412261 prove=12904
707s: mem=32431Mb trans=6702352 traceSteps=4903636 explored=6702353 saved=6519170 prove=13274
722s: mem=32462Mb trans=6809517 traceSteps=4981604 explored=6809517 saved=6622545 prove=13635
737s: mem=32462Mb trans=6924368 traceSteps=5064931 explored=6924368 saved=6732786 prove=13969
752s: mem=32488Mb trans=7041300 traceSteps=5150330 explored=7041301 saved=6846324 prove=14262
767s: mem=32476Mb trans=7201027 traceSteps=5267239 explored=7201027 saved=7001090 prove=14453
782s: mem=32476Mb trans=7364027 traceSteps=5386374 explored=7364027 saved=7158043 prove=14652
797s: mem=32494Mb trans=7514349 traceSteps=5496304 explored=7514350 saved=7303835 prove=14874
812s: mem=32483Mb trans=7682357 traceSteps=5619041 explored=7682357 saved=7466361 prove=15061
827s: mem=32510Mb trans=7845137 traceSteps=5737592 explored=7845138 saved=7622537 prove=15256
842s: mem=32510Mb trans=8000283 traceSteps=5851406 explored=8000284 saved=7773098 prove=15458
857s: mem=32502Mb trans=8165690 traceSteps=5972425 explored=8165690 saved=7933171 prove=15634
872s: mem=32528Mb trans=8345278 traceSteps=6103262 explored=8345279 saved=8104745 prove=15802
887s: mem=32520Mb trans=8505245 traceSteps=6219592 explored=8505246 saved=8257526 prove=16001
902s: mem=32544Mb trans=8688605 traceSteps=6352803 explored=8688605 saved=8431854 prove=16156
917s: mem=32544Mb trans=8816530 traceSteps=6445720 explored=8816531 saved=8554222 prove=16454
932s: mem=32536Mb trans=8919563 traceSteps=6520754 explored=8919564 saved=8653879 prove=16804
947s: mem=32536Mb trans=9023944 traceSteps=6596623 explored=9023944 saved=8754695 prove=17155
962s: mem=32559Mb trans=9133000 traceSteps=6675613 explored=9133001 saved=8858923 prove=17490
977s: mem=32559Mb trans=9240426 traceSteps=6753838 explored=9240426 saved=8962878 prove=17793
992s: mem=32551Mb trans=9376136 traceSteps=6853245 explored=9376137 saved=9094797 prove=18018
1007s: mem=32571Mb trans=9534367 traceSteps=6969156 explored=9534367 saved=9247974 prove=18194
1022s: mem=32566Mb trans=9683325 traceSteps=7078074 explored=9683326 saved=9391644 prove=18385
1037s: mem=32566Mb trans=9824194 traceSteps=7181334 explored=9824195 saved=9528333 prove=18592
1052s: mem=32582Mb trans=9983156 traceSteps=7297569 explored=9983156 saved=9681868 prove=18753
1067s: mem=32577Mb trans=10137361 traceSteps=7410112 explored=10137361 saved=9830312 prove=18935
1082s: mem=32577Mb trans=10282668 traceSteps=7516389 explored=10282669 saved=9971109 prove=19141
1097s: mem=32589Mb trans=10447796 traceSteps=7636789 explored=10447796 saved=10130226 prove=19304
1112s: mem=32586Mb trans=10614718 traceSteps=7758165 explored=10614719 saved=10289421 prove=19477
1127s: mem=32596Mb trans=10770556 traceSteps=7871676 explored=10770556 saved=10438452 prove=19657
1142s: mem=32596Mb trans=10946340 traceSteps=7999204 explored=10946340 saved=10605357 prove=19811
1157s: mem=32593Mb trans=11072841 traceSteps=8090773 explored=11072842 saved=10725520 prove=20098
1172s: mem=32603Mb trans=11215471 traceSteps=8194361 explored=11215471 saved=10861634 prove=20340
1187s: mem=32600Mb trans=11389781 traceSteps=8321122 explored=11389782 saved=11027836 prove=20488
1202s: mem=32600Mb trans=11569030 traceSteps=8451308 explored=11569030 saved=11198002 prove=20640
1217s: mem=32610Mb trans=11680595 traceSteps=8532053 explored=11680596 saved=11304235 prove=20959
1232s: mem=32607Mb trans=11828793 traceSteps=8639865 explored=11828793 saved=11445862 prove=21167
1247s: mem=32607Mb trans=11998507 traceSteps=8763227 explored=11998508 saved=11607649 prove=21322
1262s: mem=32615Mb trans=12176241 traceSteps=8892137 explored=12176241 saved=11775866 prove=21465
1277s: mem=32612Mb trans=12280374 traceSteps=8967540 explored=12280374 saved=11875299 prove=21788
1292s: mem=32612Mb trans=12430349 traceSteps=9076743 explored=12430350 saved=12018767 prove=21983
1307s: mem=32619Mb trans=12596165 traceSteps=9197412 explored=12596165 saved=12176957 prove=22135
1322s: mem=32618Mb trans=12766828 traceSteps=9321008 explored=12766829 saved=12338275 prove=22293
1337s: mem=32622Mb trans=12925208 traceSteps=9435452 explored=12925209 saved=12487597 prove=22499
1352s: mem=32622Mb trans=13079703 traceSteps=9547177 explored=13079703 saved=12633186 prove=22663
1367s: mem=32621Mb trans=13238268 traceSteps=9661823 explored=13238269 saved=12782592 prove=22827

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


=== Command ===
civl verify treebuffer-driver.cvl treebuffer-realtime.c 

=== Stats ===
   time (s)            : 1380.24
   memory (bytes)      : 34196684800
   max process count   : 1
   states              : 13392054
   states saved        : 12925711
   state matches       : 0
   transitions         : 13392053
   trace steps         : 9772336
   valid calls         : 30457806
   provers             : z3
   prover calls        : 22970

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