/opt/local/bin/civl-1.7.1 verify treebuffer-driver.cvl treebuffer-caterpillar.c
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
17s: mem=31403Mb trans=122499 traceSteps=84471 explored=122500 saved=114419 prove=431
32s: mem=31403Mb trans=252266 traceSteps=173881 explored=252266 saved=235484 prove=903
47s: mem=31403Mb trans=401181 traceSteps=276373 explored=401181 saved=374453 prove=1374
62s: mem=31403Mb trans=564881 traceSteps=389181 explored=564881 saved=528033 prove=1803
77s: mem=31403Mb trans=737516 traceSteps=508592 explored=737516 saved=689970 prove=2230
92s: mem=31403Mb trans=888494 traceSteps=612626 explored=888494 saved=830969 prove=2665
107s: mem=31403Mb trans=1024872 traceSteps=706537 explored=1024872 saved=958179 prove=3129
122s: mem=31940Mb trans=1171332 traceSteps=807527 explored=1171332 saved=1094896 prove=3573
137s: mem=31940Mb trans=1320286 traceSteps=909960 explored=1320286 saved=1233761 prove=4021
152s: mem=31863Mb trans=1455741 traceSteps=1003065 explored=1455742 saved=1360263 prove=4471
167s: mem=31863Mb trans=1596728 traceSteps=1099943 explored=1596729 saved=1491887 prove=4900
182s: mem=32041Mb trans=1736097 traceSteps=1195829 explored=1736097 saved=1622306 prove=5308
197s: mem=32041Mb trans=1865573 traceSteps=1284903 explored=1865573 saved=1743177 prove=5755
212s: mem=32026Mb trans=2006792 traceSteps=1381824 explored=2006792 saved=1875173 prove=6161
227s: mem=32092Mb trans=2149424 traceSteps=1480327 explored=2149426 saved=2009797 prove=6566
242s: mem=32092Mb trans=2294850 traceSteps=1581558 explored=2294851 saved=2148681 prove=6962
257s: mem=32078Mb trans=2432942 traceSteps=1677372 explored=2432942 saved=2279967 prove=7356
272s: mem=32078Mb trans=2572629 traceSteps=1774506 explored=2572630 saved=2412934 prove=7729
287s: mem=32071Mb trans=2711487 traceSteps=1870710 explored=2711487 saved=2544110 prove=8114
302s: mem=32071Mb trans=2847939 traceSteps=1965066 explored=2847939 saved=2672975 prove=8503
317s: mem=32075Mb trans=2982112 traceSteps=2057981 explored=2982111 saved=2800194 prove=8887
332s: mem=32075Mb trans=3107041 traceSteps=2144150 explored=3107041 saved=2917991 prove=9294
347s: mem=32086Mb trans=3232953 traceSteps=2230696 explored=3232954 saved=3035732 prove=9683
362s: mem=32086Mb trans=3352614 traceSteps=2313123 explored=3352615 saved=3147608 prove=10085
377s: mem=32078Mb trans=3478531 traceSteps=2399639 explored=3478531 saved=3265160 prove=10475
392s: mem=32122Mb trans=3604051 traceSteps=2485888 explored=3604052 saved=3382291 prove=10824
407s: mem=32122Mb trans=3728288 traceSteps=2571154 explored=3728289 saved=3498495 prove=11208
422s: mem=32122Mb trans=3853095 traceSteps=2657371 explored=3853095 saved=3616645 prove=11559
437s: mem=32109Mb trans=3977147 traceSteps=2743175 explored=3977147 saved=3733870 prove=11911
452s: mem=32109Mb trans=4097465 traceSteps=2826119 explored=4097465 saved=3847184 prove=12271
467s: mem=32158Mb trans=4208378 traceSteps=2902370 explored=4208379 saved=3950871 prove=12659
482s: mem=32158Mb trans=4326603 traceSteps=2983779 explored=4326604 saved=4061470 prove=13023
497s: mem=32138Mb trans=4438284 traceSteps=3060504 explored=4438285 saved=4165708 prove=13374
512s: mem=32138Mb trans=4550968 traceSteps=3137987 explored=4550969 saved=4270876 prove=13715
527s: mem=32196Mb trans=4664092 traceSteps=3215647 explored=4664092 saved=4376643 prove=14065
542s: mem=32196Mb trans=4787784 traceSteps=3300736 explored=4787785 saved=4492928 prove=14398
557s: mem=32176Mb trans=4902501 traceSteps=3380152 explored=4902502 saved=4601582 prove=14723
572s: mem=32176Mb trans=5013371 traceSteps=3456725 explored=5013371 saved=4706108 prove=15047
587s: mem=32176Mb trans=5120876 traceSteps=3530742 explored=5120876 saved=4807267 prove=15415
602s: mem=32238Mb trans=5242429 traceSteps=3614111 explored=5242430 saved=4920982 prove=15737
617s: mem=32238Mb trans=5354450 traceSteps=3691229 explored=5354450 saved=5026411 prove=16090
632s: mem=32217Mb trans=5466405 traceSteps=3768030 explored=5466405 saved=5131108 prove=16417
647s: mem=32217Mb trans=5577107 traceSteps=3844213 explored=5577107 saved=5235318 prove=16752
662s: mem=32282Mb trans=5686068 traceSteps=3918991 explored=5686067 saved=5337200 prove=17066
677s: mem=32282Mb trans=5793476 traceSteps=3992889 explored=5793477 saved=5438316 prove=17379
692s: mem=32282Mb trans=5902345 traceSteps=4067537 explored=5902346 saved=5540540 prove=17708
707s: mem=32260Mb trans=6011894 traceSteps=4142595 explored=6011894 saved=5643485 prove=18015

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


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

=== Stats ===
   time (s)            : 707.08
   memory (bytes)      : 33827586048
   max process count   : 1
   states              : 6020981
   states saved        : 5652046
   state matches       : 0
   transitions         : 6020980
   trace steps         : 4148802
   valid calls         : 11676678
   provers             : z3
   prover calls        : 18035

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