Test/stratifiedinline/bar12.bpl


1
2
3
4
5
6
7
8

function {:inline} f(a:bool) : bool { true }

procedure {:entrypoint} main()
{
  var x: int;
   assume f(x >= 0);
  assume x >= 0;
}