Test/inline/expansion3.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

function foo3(x:int, y:bool) returns(bool);
axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));

axiom foo3(1,false);

procedure baz1()
  requires foo3(2,false);
{
  assume foo3(1,true);
}

function x1(x:int) returns(bool);
axiom {:inline true} (forall x:int :: x1(x) <==> x > 0);
axiom {:inline true} (forall x:int :: x1(x) <==> x >= 1);

procedure bar()
{
  assert x1(3);
}