Initial set of files.

1 files changed, 19 insertions, 0 deletions

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

+}