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/aitest1/Output | 510 ----------------------------------------------------
 1 file changed, 510 deletions(-)
 delete mode 100644 Test/aitest1/Output

(limited to 'Test/aitest1')

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