summaryrefslogtreecommitdiff
path: root/Test/inline/expansion3.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/inline/expansion3.bpl')
-rw-r--r--Test/inline/expansion3.bpl12
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);
-}