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;
tff(inv0, claim, ![X1 : $int]: (bb(X1) = bb0(X1) | ~$lesseq(m,$sum(a0,sK0(X1))))).
tff(inv1, claim, ![X2 : $int]: (bb(X2) = bb0(X2) | $lesseq(0,sK0(X2)))).
tff(inv2, claim, ![X0 : $int]: (bb(X0) = bb0(X0) | $sum(a0,sK0(X0)) = X0)).
tff(inv4, claim, ~$lesseq(m,$sum(a,a0)) | $lesseq(0,a0) | ~$lesseq(0,a)).
tff(inv5, claim, ![X0 : $int,X1 : $int,X2 : $int]: ($sum(a0,sK0(X0)) != X1 | aa($sum(a0,sK0(X0))) != X2 | bb(X1) = X2 | bb(X0) = bb0(X0))).
tff(inv8, claim, $lesseq(a,$sum(1,a0)) | ~$lesseq(m,a0)).
tff(inv9, claim, $lesseq($sum(a,a0),a) | $lesseq(0,a0)).
tff(inv11, claim, ![X1 : $int]: ($lesseq($sum(a,$uminus(a0)),X1) | ~$lesseq(0,X1) | ~$lesseq(m,$sum(a0,X1)))).
tff(inv15, claim, ![X1 : $int,X2 : $int]: ($lesseq(X2,$sum(X1,$sum(a,$uminus(a0)))) | ~$lesseq(a0,X1) | ~$lesseq(X2,a))).
tff(inv17, claim, ![X2 : $int,X3 : $int]: ($lesseq(a,$sum(X2,$sum(X3,$sum(a,$uminus(a0))))) | ~$lesseq(a0,$sum(X2,X3)))).
tff(inv19, claim, ![X1 : $int,X2 : $int]: (~$lesseq(X2,$sum(X1,$sum(a,$uminus(a0)))) | ~$lesseq(X1,a0) | $lesseq(X2,a))).
tff(inv26, claim, ![X2 : $int,X3 : $int]: ($lesseq($sum(X3,$sum(a,$sum($uminus(a0),X2))),$sum(a,X2)) | ~$lesseq(X3,a0))).
tff(inv27, claim, ![X4 : $int,X5 : $int]: ($lesseq($sum(a,X4),$sum(X5,$sum(a,$sum($uminus(a0),X4)))) | ~$lesseq(a0,X5))).
tff(inv29, claim, ![X18 : $int,X19 : $int]: ($lesseq(X18,$sum(X19,$sum(a,$uminus(a0)))) | $lesseq(a,X18) | ~$lesseq(a0,X19))).
tff(inv30, claim, ![X28 : $int,X29 : $int]: ($lesseq($sum(X28,$sum(a,$uminus(a0))),X29) | $lesseq(X29,a) | ~$lesseq(X28,a0))).
tff(inv32, claim, ![X15 : $int,X16 : $int]: (~$lesseq($sum(a,$sum($uminus(a0),X15)),X16) | $lesseq($sum(a,X15),$sum(X16,a0)))).
tff(inv33, claim, ![X15 : $int,X16 : $int]: ($lesseq($sum(a,$sum($uminus(a0),$sum(X15,X16))),$sum(a,X15)) | ~$lesseq(X16,a0))).
tff(inv35, claim, ![X15 : $int,X16 : $int]: (~$lesseq(X16,$sum(a,$sum($uminus(a0),X15))) | $lesseq($sum(X16,a0),$sum(a,X15)))).
tff(inv36, claim, ![X15 : $int,X16 : $int]: ($lesseq($sum(a,X15),$sum(a,$sum($uminus(a0),$sum(X15,X16)))) | ~$lesseq(a0,X16))).
tff(inv39, claim, ![X39 : $int,X40 : $int]: ($lesseq(a,$sum(X40,$sum(X39,$sum(a,$uminus(a0))))) | ~$lesseq(a0,$sum(X39,X40)))).
tff(inv48, claim, ![X23 : $int,X24 : $int]: (~$lesseq($uminus($sum(a,$sum($uminus(a0),X23))),X24) | $lesseq($uminus($sum(a,X23)),$sum(X24,$uminus(a0))))).
tff(inv50, claim, ![X23 : $int,X24 : $int]: (~$lesseq(X24,$uminus($sum(a,$sum($uminus(a0),X23)))) | $lesseq($sum(X24,$uminus(a0)),$uminus($sum(a,X23))))).
tff(inv51, claim, ![X32 : $int,X33 : $int,X34 : $int]: ($lesseq($sum(a,X32),$sum(X33,$sum(X34,$sum(a,$sum($uminus(a0),X32))))) | ~$lesseq(a0,$sum(X33,X34)))).
tff(inv52, claim, ![X30 : $int,X31 : $int]: ($lesseq($sum(X30,$sum(a,$uminus(a0))),$sum(X31,a)) | ~$lesseq(X30,$sum(X31,a0)))).
tff(inv53, claim, ![X32 : $int,X33 : $int,X34 : $int]: ($lesseq($sum(X33,$sum(a,$sum($uminus(a0),X32))),$sum(X34,$sum(a,X32))) | ~$lesseq(X33,$sum(X34,a0)))).
tff(inv54, claim, ![X30 : $int,X31 : $int]: ($lesseq($sum(X30,a),$sum(X31,$sum(a,$uminus(a0)))) | ~$lesseq($sum(X30,a0),X31))).
tff(inv55, claim, ![X32 : $int,X33 : $int,X34 : $int]: ($lesseq($sum(X33,$sum(a,X32)),$sum(X34,$sum(a,$sum($uminus(a0),X32)))) | ~$lesseq($sum(X33,a0),X34))).
tff(inv56, claim, ![X32 : $int,X33 : $int,X34 : $int]: ($lesseq($sum(X33,$sum(X34,$sum(a,$sum($uminus(a0),X32)))),$sum(a,X32)) | ~$lesseq($sum(X33,X34),a0))).
tff(inv58, claim, ![X0 : $int]: (~$lesseq($sum(a,$uminus(a0)),sK0(X0)) | bb(X0) = bb0(X0))).
tff(inv59, claim, ![X1 : $int,X2 : $int,X3 : $int]: ($lesseq($sum(a,$uminus(a0)),X1) | ~$lesseq(0,X1) | $sum(a0,X1) != X2 | aa($sum(a0,X1)) != X3 | bb(X2) = X3)).
  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;
  }
}