Removed Output files. These are created on a local machine when the tests are run.

1 files changed, 0 insertions, 510 deletions

diff --git a/Test/aitest1/Output b/Test/aitest1/Output
deleted file mode 100644
index 4e5c8f27..00000000
--- a/Test/aitest1/Output
+++ /dev/null
@@ -1,510 +0,0 @@
--------------------- ineq.bpl --------------------

-procedure SimpleLoop();

-

-

-

-implementation SimpleLoop()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 0;

-    assume i == 0;

-    goto test;

-

-  test:  // cut point

-    assume 0 <= i;

-    assume 0 <= i;

-    goto Then, Else;

-

-  Then:

-    assume 0 <= i;

-    assume i < 10;

-    i := i + 1;

-    assume i <= 10 && 1 <= i;

-    goto test;

-

-  Else:

-    assume 0 <= i;

-    assume !(i < 10);

-    assume 10 <= i;

-    return;

-}

-

-

-

-procedure VariableBoundLoop(n: int);

-

-

-

-implementation VariableBoundLoop(n: int)

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 0;

-    assume i == 0;

-    goto test;

-

-  test:  // cut point

-    assume 0 <= i;

-    assume 0 <= i;

-    goto Then, Else;

-

-  Then:

-    assume 0 <= i;

-    assume i < n;

-    i := i + 1;

-    assume i <= n && 1 <= i;

-    goto test;

-

-  Else:

-    assume 0 <= i;

-    assume !(i < n);

-    assume n <= i && 0 <= i;

-    return;

-}

-

-

-

-procedure Foo();

-

-

-

-implementation Foo()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 3 * i + 1;

-    i := 3 * (i + 1);

-    i := 1 + 3 * i;

-    i := (i + 1) * 3;

-    assume true;

-    return;

-}

-

-

-

-procedure FooToo();

-

-

-

-implementation FooToo()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 5;

-    i := 3 * i + 1;

-    i := 3 * (i + 1);

-    i := 1 + 3 * i;

-    i := (i + 1) * 3;

-    assume 1 / 3 * i == 155;

-    return;

-}

-

-

-

-procedure FooTooStepByStep();

-

-

-

-implementation FooTooStepByStep()

-{

-  var i: int;

-

-  L0:

-    assume true;

-    i := 5;

-    assume i == 5;

-    goto L1;

-

-  L1:

-    assume i == 5;

-    i := 3 * i + 1;

-    assume i == 16;

-    goto L2;

-

-  L2:

-    assume i == 16;

-    i := 3 * (i + 1);

-    assume 1 / 3 * i == 17;

-    goto L3;

-

-  L3:

-    assume 1 / 3 * i == 17;

-    i := 1 + 3 * i;

-    assume i == 154;

-    goto L4;

-

-  L4:

-    assume i == 154;

-    i := (i + 1) * 3;

-    assume 1 / 3 * i == 155;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear0.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear1.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume x * x == y;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear2.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume x == 8;

-    assume x == 8;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear3.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume x < y;

-    assume x + 1 <= y;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear4.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-  modifies x;

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    assume x < y;

-    assume x + 1 <= y;

-    goto B;

-

-  B:

-    assume x + 1 <= y;

-    x := x * x;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear5.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-  modifies x;

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    assume 0 - 1 <= x;

-    assume -1 <= x;

-    goto B;

-

-  B:

-    assume -1 <= x;

-    assume x < y;

-    assume x + 1 <= y && -1 <= x;

-    goto C;

-

-  C:

-    assume x + 1 <= y && -1 <= x;

-    x := x * x;

-    assume 0 <= y;

-    goto D;

-

-  D:

-    assume 0 <= y;

-    x := y;

-    assume x == y && 0 <= y;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear6.bpl --------------------

-var x: int;

-

-var y: int;

-

-var z: int;

-

-procedure p();

-  modifies x;

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    x := 8;

-    assume x == 8;

-    goto B, C;

-

-  B:

-    assume x == 8;

-    x := 9;

-    assume x == 9;

-    goto D;

-

-  C:

-    assume x == 8;

-    x := 10;

-    assume x == 10;

-    goto D;

-

-  D:

-    assume 9 <= x && x <= 10;

-    assume 9 <= x && x <= 10;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear7.bpl --------------------

-var x: int;

-

-var y: int;

-

-var z: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    assume true;

-    goto B, C;

-

-  B:

-    assume true;

-    assume x <= 0;

-    assume x <= 0;

-    goto D;

-

-  C:

-    assume true;

-    assume y <= 0;

-    assume y <= 0;

-    goto D;

-

-  D:

-    assume true;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear8.bpl --------------------

-procedure foo();

-

-

-

-implementation foo()

-{

-  var i: int;

-  var j: int;

-  var n: int;

-

-  A:

-    assume true;

-    n := 0;

-    assume n == 0;

-    goto B;

-

-  B:

-    assume n == 0;

-    j := 0;

-    assume j == 0 && n == 0;

-    goto C;

-

-  C:

-    assume j == 0 && n == 0;

-    i := j + 1;

-    assume i == j + 1 && j == 0 && n == 0;

-    goto D;

-

-  D:

-    assume i == j + 1 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 2 && j == 0 && n == 0;

-    goto E;

-

-  E:

-    assume i == j + 2 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 3 && j == 0 && n == 0;

-    goto F;

-

-  F:

-    assume i == j + 3 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 4 && j == 0 && n == 0;

-    goto G;

-

-  G:

-    assume i == j + 4 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 5 && j == 0 && n == 0;

-    goto H;

-

-  H:

-    assume i == j + 5 && j == 0 && n == 0;

-    j := j + 1;

-    assume i == j + 4 && j == 1 && n == 0;

-    goto I;

-

-  I:

-    assume i == j + 4 && j == 1 && n == 0;

-    assume i == j + 4 && j == 1 && n == 0;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear9.bpl --------------------

-procedure foo();

-

-

-

-implementation foo()

-{

-  var i: int;

-  var j: int;

-  var n: int;

-

-  entry:

-    assume true;

-    assume n >= 4;

-    i := 0;

-    j := i + 1;

-    assume j == i + 1 && i == 0 && 4 <= n;

-    goto exit, loop0;

-

-  loop0:  // cut point

-    assume 4 <= n && 0 <= i && j == i + 1;

-    assume j <= n;

-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;

-    goto loop1;

-

-  loop1:

-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;

-    i := i + 1;

-    assume 1 <= i && j == i && j <= n && 4 <= n;

-    goto loop2;

-

-  loop2:

-    assume j <= n && 4 <= n && 1 <= i && j == i;

-    j := j + 1;

-    assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;

-    goto loop0, exit;

-

-  exit:

-    assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;

-    assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Bound.bpl -------------------- 

-

-Boogie program verifier finished with 1 verified, 0 errors