blob: 1c1ff51c45c5e6bdb6d2c4b0c6f34cd7f7cdd424 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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;
}
|