1 files changed, 2 insertions, 10 deletions
diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl
index 1fd3d853..2b1f0caa 100644
--- a/Test/inline/expansion3.bpl
+++ b/Test/inline/expansion3.bpl
@@ -1,5 +1,5 @@
-function foo3(x:int, y:bool) returns(bool);
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));
+function {:inline true} foo3(x:int, y:bool) returns(bool)
+ { foo3(x,y) }
 
 axiom foo3(1,false);
 
@@ -9,11 +9,3 @@ procedure baz1()
   assume foo3(1,true);
 }
 
-function x1(x:int) returns(bool);
-axiom {:inline true} (forall x:int :: x1(x) <==> x > 0);
-axiom {:inline true} (forall x:int :: x1(x) <==> x >= 1);
-
-procedure bar()
-{
-  assert x1(3);
-}