/opt/local/bin/civl-1.7.1 verify -loop  pair-insert-loop.cvl
CIVL v1.17.1 of 2018-07-30 -- http://vsl.cis.udel.edu/civl
n=X_n
k=Y4, LEFT=X_LEFT
k=Y6, LEFT=X_LEFT
k=Y2-1, LEFT=X_LEFT
k=Y4, LEFT=X_LEFT
k=Y4, LEFT=X_LEFT
k=Y6, LEFT=X_LEFT
k=Y1-1, LEFT=X_LEFT
k=Y4, LEFT=X_LEFT

=== Source files ===
pair-insert-loop.cvl  (pair-insert-loop.cvl)


=== Command ===
civl verify -loop pair-insert-loop.cvl 

=== Stats ===
   time (s)            : 15.62
   memory (bytes)      : 32928432128
   max process count   : 1
   states              : 1136
   states saved        : 915
   state matches       : 27
   transitions         : 1162
   trace steps         : 641
   valid calls         : 515
   provers             : z3
   prover calls        : 226

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