void copy(){
 // from paper by R. Jhala, CAV 2007
  int a, m;
  int *aa, *bb;

  //This is the program for which Vampire is ran
  a = 0;
  while( a < m ) {
    bb[a] = aa[a];
    a = a+1;
  }
}

void partition() { // from paper by S.Gulwani, PLDI 2006
  int a, m, b, c;
  int *aa, *bb, *cc;

  //This is the program for which Vampire is ran
  //Vampire generates invariants with quantifier alterantions
  a = 0;
  b = 0;
  c = 0;
  while ( a < m ) {
    if ( aa[a] >= 0 ) {
      bb[b] = aa[a];
      b = b+1;
    } else {
      cc[c] = aa[a];
      c = c+1;
    }
    a = a+1;
  }
}