diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/inline/expansion2.bpl | |
Initial set of files.
Diffstat (limited to 'Test/inline/expansion2.bpl')
| -rw-r--r-- | Test/inline/expansion2.bpl | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl new file mode 100644 index 00000000..fc14a0eb --- /dev/null +++ b/Test/inline/expansion2.bpl @@ -0,0 +1,14 @@ +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);
+
+axiom (forall z:int :: z>12 ==> xxgz(z));
+axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);
+
+procedure foo()
+{
+ assert xxgz(12);
+ assert xxf1(3,true) == 4;
+}
+
|