Boogie: Get rid of {:inline} attributes on axioms

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);

-}