source: CIVL/examples/languageFeatures/quantifiedComp.cvl@ 4f3a349

#include <civlc.cvh>
#include <assert.h>

$input int n=3;
$input int x;
$input int y;
$input int X1[n];

$assume (x < n && y < n && x >=0 && y>=0);

int lcp(int *arr, int n, int x, int y){
  int l=0;
  while (x+l<n && y+l<n && arr[x+l]==arr[y+l]) {
      l++;
  }
  return l;
}

void main(){
  int result = lcp(X1, n, x, y);
  assert($forall {int i | i>=0 && i<result} X1[x+i] == X1[y+i]);
}