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

1 files changed, 0 insertions, 111 deletions

diff --git a/Test/aitest0/Output b/Test/aitest0/Output
deleted file mode 100644
index 58750460..00000000
--- a/Test/aitest0/Output
+++ /dev/null
@@ -1,111 +0,0 @@
-var GlobalFlag: bool;

-

-const A: int;

-

-const B: int;

-

-const C: int;

-

-procedure Join(b: bool);

-  modifies GlobalFlag;

-

-

-

-implementation Join(b: bool)

-{

-  var x: int;

-  var y: int;

-  var z: int;

-

-  start:

-    assume true;

-    GlobalFlag := true;

-    x := 3;

-    y := 4;

-    z := x + y;

-    assume x == 3 && y == 4 && z == 7;

-    goto Then, Else;

-

-  Then:

-    assume x == 3 && y == 4 && z == 7;

-    assume b <==> true;

-    x := x + 1;

-    assume x == 4 && y == 4 && z == 7;

-    goto join;

-

-  Else:

-    assume x == 3 && y == 4 && z == 7;

-    assume b <==> false;

-    y := 4;

-    assume x == 3 && y == 4 && z == 7;

-    goto join;

-

-  join:

-    assume y == 4 && z == 7;

-    assert y == 4;

-    assert z == 7;

-    assert GlobalFlag <==> true;

-    assume y == 4 && z == 7;

-    return;

-}

-

-

-

-procedure Loop();

-

-

-

-implementation Loop()

-{

-  var c: int;

-  var i: int;

-

-  start:

-    assume true;

-    c := 0;

-    i := 0;

-    assume c == 0 && i == 0;

-    goto test;

-

-  test:  // cut point

-    assume c == 0;

-    assume c == 0;

-    goto Then, Else;

-

-  Then:

-    assume c == 0;

-    assume i < 10;

-    i := i + 1;

-    assume c == 0;

-    goto test;

-

-  Else:

-    assume c == 0;

-    assume c == 0;

-    return;

-}

-

-

-

-procedure Evaluate();

-

-

-

-implementation Evaluate()

-{

-  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 i == 465;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors