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; } }