diff options
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;
+}
|