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

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl
index fc14a0eb..b6ed19ed 100644
--- a/Test/inline/expansion2.bpl
+++ b/Test/inline/expansion2.bpl
@@ -1,7 +1,7 @@
-function xxgz(x:int) returns(bool);

-function xxf1(x:int,y:bool) returns(int);

-axiom {:inline true} (forall x:int :: xxgz(x) <==> x > 0);

-axiom {:inline true} (forall x:int, y:bool :: xxf1(x,y) == x+1);

+function {:inline true} xxgz(x:int) returns(bool)

+ { x > 0 }

+function {:inline true} xxf1(x:int,y:bool) returns(int)

+  { x + 1 }

 

 axiom (forall z:int :: z>12 ==> xxgz(z));

 axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);