/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=222715 traceSteps=153402 explored=222715 saved=210695 prove=266
32s: mem=31403Mb trans=518523 traceSteps=357891 explored=518523 saved=491556 prove=534
47s: mem=31403Mb trans=809772 traceSteps=559415 explored=809772 saved=769375 prove=811
62s: mem=31403Mb trans=1085227 traceSteps=749179 explored=1085228 saved=1030805 prove=1105
77s: mem=31403Mb trans=1365795 traceSteps=943101 explored=1365795 saved=1298174 prove=1372
92s: mem=31800Mb trans=1635542 traceSteps=1129415 explored=1635543 saved=1556208 prove=1677

=== 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)            : 101.52
   memory (bytes)      : 33279705088
   max process count   : 1
   states              : 1795270
   states saved        : 1707935
   state matches       : 0
   transitions         : 1795269
   trace steps         : 1238726
   valid calls         : 2941340
   provers             : z3
   prover calls        : 1945

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