1 files changed, 0 insertions, 33 deletions
diff --git a/Test/inline/expansion.bpl b/Test/inline/expansion.bpl
deleted file mode 100644
index 41acfb44..00000000
--- a/Test/inline/expansion.bpl
+++ /dev/null
@@ -1,33 +0,0 @@
-const q : int;
-const p : bool;
-function foo(x:int, y:bool) returns(bool);
-function foo1(x:int, y:bool) returns(bool);
-function foo2(x:int, y:bool) returns(bool);
-function foo3(x:int, y:bool) returns(bool);
-// OK
-axiom {:inline false} (forall x:int, y:bool :: foo(x,p) <==> x > 10 && y);
-axiom {:inline true} (forall x:int, y:bool :: foo1(x,y) == (x > 10 && y));
-axiom {:inline true} (forall x:int, y:bool :: foo2(x,y) == (q > 10 && y));
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));
-// fail
-axiom {:inline 1} (forall x:int, y:bool :: foo(x,y) <==> x > 10 && y);
-axiom {:inline true} (forall x:int, y:bool :: foo(x,p) <==> x > 10 && y);
-axiom {:inline true} (forall y:bool :: foo(q,y) == (q > 10 && y));
-axiom {:inline true} (forall x:int, y:bool, z:int :: foo(x,y) == (q > 10 && y));
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == (q > 10 && y));
-axiom {:inline true} true;
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,true) == (q > 10 && y));
-
-
-procedure baz1()
-{
-  assert foo3(1,true);
-}
-
-procedure baz2()
-{
-  assert foo1(true,true);
-}
-
-function foo4(x:int, y:int) returns(bool);
-axiom {:inline true} (forall x:int,z:int :: foo4(x,x) == (x > 0));