CIVL v1.17.1+ of 2018-07-30 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 29:
CIVL execution violation in p0 (kind: OUT_OF_BOUNDS, certainty: PROVEABLE)
at pair-insert-bad.cvl:25.16-21
    while (a1 < a[--k]) a[k + 2] = a[k];
                ^^^^^^

possible negative array index: -1

Input:
  n=5
  N=5
  LEFT=0
  RIGHT=4
  A=X_A
Context:
  (OUT_OF_BOUND(X_A,-1)+(-1*X_A[1]))<=0
  (OUT_OF_BOUND(X_A,-1)+(-1*X_A[2]))<=0
  (OUT_OF_BOUND(X_A,-1)+(-1*X_A[3]))<=0
  (OUT_OF_BOUND(X_A,-1)+(-1*X_A[4]))<=0
  (OUT_OF_BOUND(X_A,-1)+(-1*X_A[0]))<=0
  0<=(X_A[1]+(-1*X_A[0])-1)
Call stacks:
process 0:
  main at pair-insert-bad.cvl:25.11-12 "a1"

Logging new entry 0, writing trace to CIVLREP/pair-insert-bad_0.trace
Terminating search after finding 1 violation.

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


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

=== Stats ===
   time (s)            : 1.23
   memory (bytes)      : 2058354688
   max process count   : 1
   states              : 54
   states saved        : 41
   state matches       : 0
   transitions         : 54
   trace steps         : 28
   valid calls         : 86
   provers             : z3
   prover calls        : 26

=== Result ===
The program MAY NOT be correct.  See CIVLREP/pair-insert-bad_log.txt
