From faf1c46b1e67ab4c3d8a1c82974b0499015a83d3 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 7 Aug 2009 17:21:13 +0000
Subject: Removed Output files.  These are created on a local machine when the
 tests are run.

---
 Test/aitest0/Output | 111 ----------------------------------------------------
 1 file changed, 111 deletions(-)
 delete mode 100644 Test/aitest0/Output

(limited to 'Test/aitest0')

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
-- 
cgit v1.2.3