/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=110162 traceSteps=75849 explored=110162 saved=102865 prove=502
32s: mem=31403Mb trans=235577 traceSteps=162168 explored=235577 saved=220748 prove=984
47s: mem=31403Mb trans=370624 traceSteps=255191 explored=370625 saved=347787 prove=1507
62s: mem=31403Mb trans=501692 traceSteps=345259 explored=501692 saved=470869 prove=2008
77s: mem=31403Mb trans=630538 traceSteps=433557 explored=630538 saved=591738 prove=2535

=== 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)            : 85.43
   memory (bytes)      : 32928432128
   max process count   : 1
   states              : 696133
   states saved        : 653342
   state matches       : 0
   transitions         : 696132
   trace steps         : 478517
   valid calls         : 1377365
   provers             : z3
   prover calls        : 2912

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