From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Test/inline/expansion3.bpl | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 Test/inline/expansion3.bpl

(limited to 'Test/inline/expansion3.bpl')

diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl
new file mode 100644
index 00000000..1fd3d853
--- /dev/null
+++ b/Test/inline/expansion3.bpl
@@ -0,0 +1,19 @@
+function foo3(x:int, y:bool) returns(bool);
+axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));
+
+axiom foo3(1,false);
+
+procedure baz1()
+  requires foo3(2,false);
+{
+  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);
+}
-- 
cgit v1.2.3