1 files changed, 0 insertions, 134 deletions
diff --git a/Test/test2/CallForall.bpl b/Test/test2/CallForall.bpl
deleted file mode 100644
index 98a62103..00000000
--- a/Test/test2/CallForall.bpl
+++ /dev/null
@@ -1,134 +0,0 @@
-function G(int) returns (int);
-axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x);
-
-function F(int) returns (int);
-axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5);
-
-procedure Lemma(y: int)
-  requires 0 <= y;
-  ensures F(y) == 5;
-{
-  // proof:
-  assert G(y) == y;
-}
-
-procedure Main0()
-{
-  assert F(2) == 5;  // error: cannot prove this directly, because of the trigger
-}
-
-procedure Main1()
-{
-  call Lemma(2);
-  assert F(2) == 5;
-}
-
-procedure Main2()
-{
-  call Lemma(3);
-  assert F(2) == 5;  // error: Lemma was instantiated the wrong way
-}
-
-procedure Main3()
-{
-  call forall Lemma(*);
-  assert F(2) == 5;
-}
-
-procedure Main4()
-{
-  call forall Lemma(*);
-  assert false;  // error
-}
-
-procedure Main5(z: int)
-{
-  call forall Lemma(*);
-  assert F(z) == 5;  // error: z might be negative
-}
-
-procedure Main6(z: int)
-  requires 0 <= z;
-{
-  call forall Lemma(*);
-  assert F(z) == 5;
-}
-
-// ------------ several parameters
-
-function K(int, int) returns (int);
-axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25);
-
-procedure MultivarLemma(x: int, y: int)
-  requires 0 <= x;
-  requires 0 <= y;
-  ensures K(x,y) == 25;
-{
-  // proof:
-  assert G(x) == x;
-  assert G(y) == y;
-}
-
-procedure Multi0(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  assert K(x,y) == 25;  // error
-}
-
-procedure Multi1(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call MultivarLemma(x, y);
-  assert K(x,y) == 25;
-}
-
-procedure Multi2(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(x, y);
-  assert K(x,y) == 25;
-}
-
-procedure Multi3(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(*, y);
-  assert K(x,y) == 25;
-}
-
-procedure Multi4(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(x, *);
-  assert K(x,y) == 25;
-}
-
-procedure Multi5(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(2 + 100, *);
-  assert K(102, y) == 25;
-  assert false;  // error
-}
-
-procedure Multi6(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(*, y);
-  assert K(x+2,y+2) == 25;  // error
-}
-
-procedure Multi7(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(x, *);
-  assert K(x+2,y+2) == 25;  // error
-}
-
-procedure Multi8(x: int, y: int)
-  requires 0 <= x && 0 <= y;
-{
-  call forall MultivarLemma(*, *);
-  assert K(x+2,y+2) == 25;  // that's the ticket!
-}
-