/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=89838 traceSteps=65434 explored=89839 saved=87683 prove=439
32s: mem=31403Mb trans=191394 traceSteps=139295 explored=191394 saved=186223 prove=858
47s: mem=31403Mb trans=331114 traceSteps=241604 explored=331114 saved=322960 prove=1203
62s: mem=31403Mb trans=495543 traceSteps=361735 explored=495543 saved=483276 prove=1515
77s: mem=31403Mb trans=676114 traceSteps=492968 explored=676114 saved=656322 prove=1793
92s: mem=31403Mb trans=819160 traceSteps=596875 explored=819160 saved=793987 prove=2151
107s: mem=31403Mb trans=969527 traceSteps=705990 explored=969528 saved=937929 prove=2492
122s: mem=31882Mb trans=1145610 traceSteps=833960 explored=1145611 saved=1106611 prove=2748
137s: mem=31806Mb trans=1307424 traceSteps=950949 explored=1307424 saved=1260010 prove=3038
152s: mem=31992Mb trans=1449009 traceSteps=1053157 explored=1449009 saved=1394504 prove=3418

=== 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)            : 168.55
   memory (bytes)      : 33546567680
   max process count   : 1
   states              : 1579100
   states saved        : 1518146
   state matches       : 0
   transitions         : 1579099
   trace steps         : 1146908
   valid calls         : 3581452
   provers             : z3
   prover calls        : 3809

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