diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-27 19:12:06 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-27 19:12:06 -0700 |
| commit | bed18114957f4e873e5055b93572a07c10e776fa (patch) | |
| tree | edb07e52cfdf438a2faf395e9439bd376ca8a691 /Test/inline/expansion4.bpl | |
| parent | a8c04614ad34b4a36c1c739f8838fe4fd6232720 (diff) | |
Boogie: Get rid of {:inline} attributes on axioms
Diffstat (limited to 'Test/inline/expansion4.bpl')
| -rw-r--r-- | Test/inline/expansion4.bpl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl new file mode 100644 index 00000000..be11a391 --- /dev/null +++ b/Test/inline/expansion4.bpl @@ -0,0 +1,9 @@ +function foo(x:int) : int
+ { if x <= 0 then 1 else foo(x - 1) + 2 }
+
+procedure bar()
+{
+ assert foo(0) == 1;
+ assert foo(1) == 3;
+ assert foo(2) == 5;
+}
|