Test/inline/expansion4.bpl


1
2
3
4
5
6
7
8
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;
}