-------------------- test0.bpl --------------------
test0.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
    test0.bpl(26,3): anon0
    test0.bpl(30,5): anon3_Then

Boogie program verifier finished with 1 verified, 1 error
-------------------- test1.bpl --------------------

procedure Main();



implementation Main()
{
  var x: int;
  var y: int;

  anon0:
    x := 1;
    y := 0;
    call x := inc(x, 5);
    call y := incdec(x, 2);
    assert x - 1 == y;
    return;
}



procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
  ensures z == x + 1 - y;



implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{

  anon0:
    z := x;
    z := x + 1;
    call z := dec(z, y);
    return;
}



procedure {:inline 1} inc(x: int, i: int) returns (y: int);
  ensures y == x + i;



implementation {:inline 1} inc(x: int, i: int) returns (y: int)
{

  anon0:
    y := x;
    y := x + i;
    return;
}



procedure {:inline 1} dec(x: int, i: int) returns (y: int);
  ensures y == x - i;



implementation {:inline 1} dec(x: int, i: int) returns (y: int)
{

  anon0:
    y := x;
    y := x - i;
    return;
}


after inlining procedure calls
procedure Main();


implementation Main()
{
  var x: int;
  var y: int;
  var inline$inc$0$x: int;
  var inline$inc$0$i: int;
  var inline$inc$0$y: int;
  var inline$incdec$0$x: int;
  var inline$incdec$0$y: int;
  var inline$incdec$0$z: int;
  var inline$dec$0$x: int;
  var inline$dec$0$i: int;
  var inline$dec$0$y: int;

  anon0:
    x := 1;
    y := 0;
    goto inline$inc$0$Entry;

  inline$inc$0$Entry:
    inline$inc$0$x := x;
    inline$inc$0$i := 5;
    goto inline$inc$0$anon0;

  inline$inc$0$anon0:
    inline$inc$0$y := inline$inc$0$x;
    inline$inc$0$y := inline$inc$0$x + inline$inc$0$i;
    goto inline$inc$0$Return;

  inline$inc$0$Return:
    assert inline$inc$0$y == inline$inc$0$x + inline$inc$0$i;
    x := inline$inc$0$y;
    goto anon0$1;

  anon0$1:
    goto inline$incdec$0$Entry;

  inline$incdec$0$Entry:
    inline$incdec$0$x := x;
    inline$incdec$0$y := 2;
    goto inline$incdec$0$anon0;

  inline$incdec$0$anon0:
    inline$incdec$0$z := inline$incdec$0$x;
    inline$incdec$0$z := inline$incdec$0$x + 1;
    goto inline$dec$0$Entry;

  inline$dec$0$Entry:
    inline$dec$0$x := inline$incdec$0$z;
    inline$dec$0$i := inline$incdec$0$y;
    goto inline$dec$0$anon0;

  inline$dec$0$anon0:
    inline$dec$0$y := inline$dec$0$x;
    inline$dec$0$y := inline$dec$0$x - inline$dec$0$i;
    goto inline$dec$0$Return;

  inline$dec$0$Return:
    assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i;
    inline$incdec$0$z := inline$dec$0$y;
    goto inline$incdec$0$anon0$1;

  inline$incdec$0$anon0$1:
    goto inline$incdec$0$Return;

  inline$incdec$0$Return:
    assert inline$incdec$0$z == inline$incdec$0$x + 1 - inline$incdec$0$y;
    y := inline$incdec$0$z;
    goto anon0$2;

  anon0$2:
    assert x - 1 == y;
    return;
}


after inlining procedure calls
procedure {:inline 1} incdec(x: int, y: int) returns (z: int);
  ensures z == x + 1 - y;


implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
  var inline$dec$0$x: int;
  var inline$dec$0$i: int;
  var inline$dec$0$y: int;

  anon0:
    z := x;
    z := x + 1;
    goto inline$dec$0$Entry;

  inline$dec$0$Entry:
    inline$dec$0$x := z;
    inline$dec$0$i := y;
    goto inline$dec$0$anon0;

  inline$dec$0$anon0:
    inline$dec$0$y := inline$dec$0$x;
    inline$dec$0$y := inline$dec$0$x - inline$dec$0$i;
    goto inline$dec$0$Return;

  inline$dec$0$Return:
    assert inline$dec$0$y == inline$dec$0$x - inline$dec$0$i;
    z := inline$dec$0$y;
    goto anon0$1;

  anon0$1:
    return;
}



Boogie program verifier finished with 4 verified, 0 errors
-------------------- test2.bpl --------------------

var glb: int;

procedure calculate();
  modifies glb;



implementation calculate()
{
  var x: int;
  var y: int;

  anon0:
    y := 5;
    call x := increase(y);
    return;
}



procedure {:inline 1} increase(i: int) returns (k: int);
  modifies glb;



implementation {:inline 1} increase(i: int) returns (k: int)
{
  var j: int;

  anon0:
    j := i;
    j := j + 1;
    glb := glb + j;
    k := j;
    return;
}


after inlining procedure calls
procedure calculate();
  modifies glb;


implementation calculate()
{
  var x: int;
  var y: int;
  var inline$increase$0$j: int;
  var inline$increase$0$i: int;
  var inline$increase$0$k: int;
  var inline$increase$0$glb: int;

  anon0:
    y := 5;
    goto inline$increase$0$Entry;

  inline$increase$0$Entry:
    inline$increase$0$i := y;
    inline$increase$0$glb := glb;
    goto inline$increase$0$anon0;

  inline$increase$0$anon0:
    inline$increase$0$j := inline$increase$0$i;
    inline$increase$0$j := inline$increase$0$j + 1;
    glb := glb + inline$increase$0$j;
    inline$increase$0$k := inline$increase$0$j;
    goto inline$increase$0$Return;

  inline$increase$0$Return:
    x := inline$increase$0$k;
    goto anon0$1;

  anon0$1:
    return;
}



Boogie program verifier finished with 2 verified, 0 errors
-------------------- test3.bpl --------------------

var glb: int;

procedure recursivetest();
  modifies glb;



implementation recursivetest()
{

  anon0:
    glb := 5;
    call glb := recursive(glb);
    return;
}



procedure {:inline 3} recursive(x: int) returns (y: int);



implementation {:inline 3} recursive(x: int) returns (y: int)
{
  var k: int;

  anon0:
    goto anon3_Then, anon3_Else;

  anon3_Then:
    assume {:partition} x == 0;
    y := 1;
    return;

  anon3_Else:
    assume {:partition} x != 0;
    goto anon2;

  anon2:
    call k := recursive(x - 1);
    y := y + k;
    return;
}


after inlining procedure calls
procedure recursivetest();
  modifies glb;


implementation recursivetest()
{
  var inline$recursive$0$k: int;
  var inline$recursive$0$x: int;
  var inline$recursive$0$y: int;
  var inline$recursive$1$k: int;
  var inline$recursive$1$x: int;
  var inline$recursive$1$y: int;
  var inline$recursive$2$k: int;
  var inline$recursive$2$x: int;
  var inline$recursive$2$y: int;

  anon0:
    glb := 5;
    goto inline$recursive$0$Entry;

  inline$recursive$0$Entry:
    inline$recursive$0$x := glb;
    goto inline$recursive$0$anon0;

  inline$recursive$0$anon0:
    goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

  inline$recursive$0$anon3_Then:
    assume {:partition} inline$recursive$0$x == 0;
    inline$recursive$0$y := 1;
    goto inline$recursive$0$Return;

  inline$recursive$0$anon3_Else:
    assume {:partition} inline$recursive$0$x != 0;
    goto inline$recursive$1$Entry;

  inline$recursive$1$Entry:
    inline$recursive$1$x := inline$recursive$0$x - 1;
    goto inline$recursive$1$anon0;

  inline$recursive$1$anon0:
    goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

  inline$recursive$1$anon3_Then:
    assume {:partition} inline$recursive$1$x == 0;
    inline$recursive$1$y := 1;
    goto inline$recursive$1$Return;

  inline$recursive$1$anon3_Else:
    assume {:partition} inline$recursive$1$x != 0;
    goto inline$recursive$2$Entry;

  inline$recursive$2$Entry:
    inline$recursive$2$x := inline$recursive$1$x - 1;
    goto inline$recursive$2$anon0;

  inline$recursive$2$anon0:
    goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

  inline$recursive$2$anon3_Then:
    assume {:partition} inline$recursive$2$x == 0;
    inline$recursive$2$y := 1;
    goto inline$recursive$2$Return;

  inline$recursive$2$anon3_Else:
    assume {:partition} inline$recursive$2$x != 0;
    call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
    inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
    goto inline$recursive$2$Return;

  inline$recursive$2$Return:
    inline$recursive$1$k := inline$recursive$2$y;
    goto inline$recursive$1$anon3_Else$1;

  inline$recursive$1$anon3_Else$1:
    inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
    goto inline$recursive$1$Return;

  inline$recursive$1$Return:
    inline$recursive$0$k := inline$recursive$1$y;
    goto inline$recursive$0$anon3_Else$1;

  inline$recursive$0$anon3_Else$1:
    inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
    goto inline$recursive$0$Return;

  inline$recursive$0$Return:
    glb := inline$recursive$0$y;
    goto anon0$1;

  anon0$1:
    return;
}


after inlining procedure calls
procedure {:inline 3} recursive(x: int) returns (y: int);


implementation {:inline 3} recursive(x: int) returns (y: int)
{
  var k: int;
  var inline$recursive$0$k: int;
  var inline$recursive$0$x: int;
  var inline$recursive$0$y: int;
  var inline$recursive$1$k: int;
  var inline$recursive$1$x: int;
  var inline$recursive$1$y: int;
  var inline$recursive$2$k: int;
  var inline$recursive$2$x: int;
  var inline$recursive$2$y: int;

  anon0:
    goto anon3_Then, anon3_Else;

  anon3_Then:
    assume {:partition} x == 0;
    y := 1;
    return;

  anon3_Else:
    assume {:partition} x != 0;
    goto inline$recursive$0$Entry;

  inline$recursive$0$Entry:
    inline$recursive$0$x := x - 1;
    goto inline$recursive$0$anon0;

  inline$recursive$0$anon0:
    goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

  inline$recursive$0$anon3_Then:
    assume {:partition} inline$recursive$0$x == 0;
    inline$recursive$0$y := 1;
    goto inline$recursive$0$Return;

  inline$recursive$0$anon3_Else:
    assume {:partition} inline$recursive$0$x != 0;
    goto inline$recursive$1$Entry;

  inline$recursive$1$Entry:
    inline$recursive$1$x := inline$recursive$0$x - 1;
    goto inline$recursive$1$anon0;

  inline$recursive$1$anon0:
    goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

  inline$recursive$1$anon3_Then:
    assume {:partition} inline$recursive$1$x == 0;
    inline$recursive$1$y := 1;
    goto inline$recursive$1$Return;

  inline$recursive$1$anon3_Else:
    assume {:partition} inline$recursive$1$x != 0;
    goto inline$recursive$2$Entry;

  inline$recursive$2$Entry:
    inline$recursive$2$x := inline$recursive$1$x - 1;
    goto inline$recursive$2$anon0;

  inline$recursive$2$anon0:
    goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

  inline$recursive$2$anon3_Then:
    assume {:partition} inline$recursive$2$x == 0;
    inline$recursive$2$y := 1;
    goto inline$recursive$2$Return;

  inline$recursive$2$anon3_Else:
    assume {:partition} inline$recursive$2$x != 0;
    call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
    inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
    goto inline$recursive$2$Return;

  inline$recursive$2$Return:
    inline$recursive$1$k := inline$recursive$2$y;
    goto inline$recursive$1$anon3_Else$1;

  inline$recursive$1$anon3_Else$1:
    inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
    goto inline$recursive$1$Return;

  inline$recursive$1$Return:
    inline$recursive$0$k := inline$recursive$1$y;
    goto inline$recursive$0$anon3_Else$1;

  inline$recursive$0$anon3_Else$1:
    inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
    goto inline$recursive$0$Return;

  inline$recursive$0$Return:
    k := inline$recursive$0$y;
    goto anon3_Else$1;

  anon3_Else$1:
    y := y + k;
    return;
}



Boogie program verifier finished with 2 verified, 0 errors
-------------------- test4.bpl --------------------

procedure main(x: int);



implementation main(x: int)
{
  var A: [int]int;
  var i: int;
  var b: bool;
  var size: int;

  anon0:
    call i, b := find(A, size, x);
    goto anon3_Then, anon3_Else;

  anon3_Then:
    assume {:partition} b;
    assert i > 0 && A[i] == x;
    goto anon2;

  anon3_Else:
    assume {:partition} !b;
    goto anon2;

  anon2:
    return;
}



procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);



implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
  var i: int;
  var b: bool;

  anon0:
    ret := 0 - 1;
    b := false;
    found := b;
    i := 0;
    goto anon4_LoopHead;

  anon4_LoopHead:
    goto anon4_LoopDone, anon4_LoopBody;

  anon4_LoopBody:
    assume {:partition} i < size;
    call b := check(A, i, x);
    goto anon5_Then, anon5_Else;

  anon5_Then:
    assume {:partition} b;
    ret := i;
    found := b;
    goto anon3;

  anon5_Else:
    assume {:partition} !b;
    goto anon4_LoopHead;

  anon4_LoopDone:
    assume {:partition} size <= i;
    goto anon3;

  anon3:
    return;
}



procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool);
  requires i >= 0;
  ensures old(A[i]) > c ==> ret == true;



implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)
{

  anon0:
    goto anon4_Then, anon4_Else;

  anon4_Then:
    assume {:partition} A[i] == c;
    ret := true;
    goto anon3;

  anon4_Else:
    assume {:partition} A[i] != c;
    ret := false;
    goto anon3;

  anon3:
    return;
}


after inlining procedure calls
procedure main(x: int);


implementation main(x: int)
{
  var A: [int]int;
  var i: int;
  var b: bool;
  var size: int;
  var inline$find$0$i: int;
  var inline$find$0$b: bool;
  var inline$find$0$A: [int]int;
  var inline$find$0$size: int;
  var inline$find$0$x: int;
  var inline$find$0$ret: int;
  var inline$find$0$found: bool;
  var inline$check$0$A: [int]int;
  var inline$check$0$i: int;
  var inline$check$0$c: int;
  var inline$check$0$ret: bool;

  anon0:
    goto inline$find$0$Entry;

  inline$find$0$Entry:
    inline$find$0$A := A;
    inline$find$0$size := size;
    inline$find$0$x := x;
    goto inline$find$0$anon0;

  inline$find$0$anon0:
    inline$find$0$ret := 0 - 1;
    inline$find$0$b := false;
    inline$find$0$found := inline$find$0$b;
    inline$find$0$i := 0;
    goto inline$find$0$anon4_LoopHead;

  inline$find$0$anon4_LoopHead:
    goto inline$find$0$anon4_LoopDone, inline$find$0$anon4_LoopBody;

  inline$find$0$anon4_LoopBody:
    assume {:partition} inline$find$0$i < inline$find$0$size;
    goto inline$check$0$Entry;

  inline$check$0$Entry:
    inline$check$0$A := inline$find$0$A;
    inline$check$0$i := inline$find$0$i;
    inline$check$0$c := inline$find$0$x;
    assert inline$check$0$i >= 0;
    goto inline$check$0$anon0;

  inline$check$0$anon0:
    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

  inline$check$0$anon4_Then:
    assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c;
    inline$check$0$ret := true;
    goto inline$check$0$anon3;

  inline$check$0$anon4_Else:
    assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;
    inline$check$0$ret := false;
    goto inline$check$0$anon3;

  inline$check$0$anon3:
    goto inline$check$0$Return;

  inline$check$0$Return:
    assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true);
    inline$find$0$b := inline$check$0$ret;
    goto inline$find$0$anon4_LoopBody$1;

  inline$find$0$anon4_LoopBody$1:
    goto inline$find$0$anon5_Then, inline$find$0$anon5_Else;

  inline$find$0$anon5_Then:
    assume {:partition} inline$find$0$b;
    inline$find$0$ret := inline$find$0$i;
    inline$find$0$found := inline$find$0$b;
    goto inline$find$0$anon3;

  inline$find$0$anon5_Else:
    assume {:partition} !inline$find$0$b;
    goto inline$find$0$anon4_LoopHead;

  inline$find$0$anon4_LoopDone:
    assume {:partition} inline$find$0$size <= inline$find$0$i;
    goto inline$find$0$anon3;

  inline$find$0$anon3:
    goto inline$find$0$Return;

  inline$find$0$Return:
    i := inline$find$0$ret;
    b := inline$find$0$found;
    goto anon0$1;

  anon0$1:
    goto anon3_Then, anon3_Else;

  anon3_Then:
    assume {:partition} b;
    assert i > 0 && A[i] == x;
    goto anon2;

  anon3_Else:
    assume {:partition} !b;
    goto anon2;

  anon2:
    return;
}


after inlining procedure calls
procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);


implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
  var i: int;
  var b: bool;
  var inline$check$0$A: [int]int;
  var inline$check$0$i: int;
  var inline$check$0$c: int;
  var inline$check$0$ret: bool;

  anon0:
    ret := 0 - 1;
    b := false;
    found := b;
    i := 0;
    goto anon4_LoopHead;

  anon4_LoopHead:
    goto anon4_LoopDone, anon4_LoopBody;

  anon4_LoopBody:
    assume {:partition} i < size;
    goto inline$check$0$Entry;

  inline$check$0$Entry:
    inline$check$0$A := A;
    inline$check$0$i := i;
    inline$check$0$c := x;
    assert inline$check$0$i >= 0;
    goto inline$check$0$anon0;

  inline$check$0$anon0:
    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

  inline$check$0$anon4_Then:
    assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c;
    inline$check$0$ret := true;
    goto inline$check$0$anon3;

  inline$check$0$anon4_Else:
    assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;
    inline$check$0$ret := false;
    goto inline$check$0$anon3;

  inline$check$0$anon3:
    goto inline$check$0$Return;

  inline$check$0$Return:
    assert inline$check$0$A[inline$check$0$i] > inline$check$0$c ==> (inline$check$0$ret <==> true);
    b := inline$check$0$ret;
    goto anon4_LoopBody$1;

  anon4_LoopBody$1:
    goto anon5_Then, anon5_Else;

  anon5_Then:
    assume {:partition} b;
    ret := i;
    found := b;
    goto anon3;

  anon5_Else:
    assume {:partition} !b;
    goto anon4_LoopHead;

  anon4_LoopDone:
    assume {:partition} size <= i;
    goto anon3;

  anon3:
    return;
}


<console>(68,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
    <console>(19,0): anon0
    <console>(28,0): inline$find$0$anon0
    <console>(38,0): inline$find$0$anon4_LoopBody
    <console>(42,0): inline$check$0$Entry
    <console>(57,0): inline$check$0$anon4_Else
    <console>(62,0): inline$check$0$anon3
    <console>(65,0): inline$check$0$Return
<console>(100,4): Error BP5001: This assertion might not hold.
Execution trace:
    <console>(19,0): anon0
    <console>(28,0): inline$find$0$anon0
    <console>(38,0): inline$find$0$anon4_LoopBody
    <console>(42,0): inline$check$0$Entry
    <console>(52,0): inline$check$0$anon4_Then
    <console>(65,0): inline$check$0$Return
    <console>(73,0): inline$find$0$anon5_Then
    <console>(87,0): inline$find$0$anon3
    <console>(90,0): inline$find$0$Return
    <console>(95,0): anon0$1
    <console>(98,0): anon3_Then
<console>(50,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
    <console>(10,0): anon0
    <console>(20,0): anon4_LoopBody
    <console>(24,0): inline$check$0$Entry
    <console>(39,0): inline$check$0$anon4_Else
    <console>(44,0): inline$check$0$anon3
    <console>(47,0): inline$check$0$Return
<console>(99,0): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
    <console>(85,0): anon0
    <console>(93,0): anon4_Else
    <console>(98,0): anon3

Boogie program verifier finished with 0 verified, 4 errors
-------------------- test6.bpl --------------------

procedure {:inline 2} foo();
  modifies x;



implementation {:inline 2} foo()
{

  anon0:
    x := x + 1;
    call foo();
    return;
}



procedure {:inline 2} foo1();
  modifies x;



implementation {:inline 2} foo1()
{

  anon0:
    x := x + 1;
    call foo2();
    return;
}



procedure {:inline 2} foo2();
  modifies x;



implementation {:inline 2} foo2()
{

  anon0:
    x := x + 1;
    call foo3();
    return;
}



procedure {:inline 2} foo3();
  modifies x;



implementation {:inline 2} foo3()
{

  anon0:
    x := x + 1;
    call foo1();
    return;
}



var x: int;

procedure bar();
  modifies x;



implementation bar()
{

  anon0:
    call foo();
    call foo1();
    return;
}


after inlining procedure calls
procedure {:inline 2} foo();
  modifies x;


implementation {:inline 2} foo()
{
  var inline$foo$0$x: int;
  var inline$foo$1$x: int;

  anon0:
    x := x + 1;
    goto inline$foo$0$Entry;

  inline$foo$0$Entry:
    inline$foo$0$x := x;
    goto inline$foo$0$anon0;

  inline$foo$0$anon0:
    x := x + 1;
    goto inline$foo$1$Entry;

  inline$foo$1$Entry:
    inline$foo$1$x := x;
    goto inline$foo$1$anon0;

  inline$foo$1$anon0:
    x := x + 1;
    call foo();
    goto inline$foo$1$Return;

  inline$foo$1$Return:
    goto inline$foo$0$anon0$1;

  inline$foo$0$anon0$1:
    goto inline$foo$0$Return;

  inline$foo$0$Return:
    goto anon0$1;

  anon0$1:
    return;
}


after inlining procedure calls
procedure {:inline 2} foo1();
  modifies x;


implementation {:inline 2} foo1()
{
  var inline$foo2$0$x: int;
  var inline$foo3$0$x: int;
  var inline$foo1$0$x: int;
  var inline$foo2$1$x: int;
  var inline$foo3$1$x: int;
  var inline$foo1$1$x: int;

  anon0:
    x := x + 1;
    goto inline$foo2$0$Entry;

  inline$foo2$0$Entry:
    inline$foo2$0$x := x;
    goto inline$foo2$0$anon0;

  inline$foo2$0$anon0:
    x := x + 1;
    goto inline$foo3$0$Entry;

  inline$foo3$0$Entry:
    inline$foo3$0$x := x;
    goto inline$foo3$0$anon0;

  inline$foo3$0$anon0:
    x := x + 1;
    goto inline$foo1$0$Entry;

  inline$foo1$0$Entry:
    inline$foo1$0$x := x;
    goto inline$foo1$0$anon0;

  inline$foo1$0$anon0:
    x := x + 1;
    goto inline$foo2$1$Entry;

  inline$foo2$1$Entry:
    inline$foo2$1$x := x;
    goto inline$foo2$1$anon0;

  inline$foo2$1$anon0:
    x := x + 1;
    goto inline$foo3$1$Entry;

  inline$foo3$1$Entry:
    inline$foo3$1$x := x;
    goto inline$foo3$1$anon0;

  inline$foo3$1$anon0:
    x := x + 1;
    goto inline$foo1$1$Entry;

  inline$foo1$1$Entry:
    inline$foo1$1$x := x;
    goto inline$foo1$1$anon0;

  inline$foo1$1$anon0:
    x := x + 1;
    call foo2();
    goto inline$foo1$1$Return;

  inline$foo1$1$Return:
    goto inline$foo3$1$anon0$1;

  inline$foo3$1$anon0$1:
    goto inline$foo3$1$Return;

  inline$foo3$1$Return:
    goto inline$foo2$1$anon0$1;

  inline$foo2$1$anon0$1:
    goto inline$foo2$1$Return;

  inline$foo2$1$Return:
    goto inline$foo1$0$anon0$1;

  inline$foo1$0$anon0$1:
    goto inline$foo1$0$Return;

  inline$foo1$0$Return:
    goto inline$foo3$0$anon0$1;

  inline$foo3$0$anon0$1:
    goto inline$foo3$0$Return;

  inline$foo3$0$Return:
    goto inline$foo2$0$anon0$1;

  inline$foo2$0$anon0$1:
    goto inline$foo2$0$Return;

  inline$foo2$0$Return:
    goto anon0$1;

  anon0$1:
    return;
}


after inlining procedure calls
procedure {:inline 2} foo2();
  modifies x;


implementation {:inline 2} foo2()
{
  var inline$foo3$0$x: int;
  var inline$foo1$0$x: int;
  var inline$foo2$0$x: int;
  var inline$foo3$1$x: int;
  var inline$foo1$1$x: int;
  var inline$foo2$1$x: int;

  anon0:
    x := x + 1;
    goto inline$foo3$0$Entry;

  inline$foo3$0$Entry:
    inline$foo3$0$x := x;
    goto inline$foo3$0$anon0;

  inline$foo3$0$anon0:
    x := x + 1;
    goto inline$foo1$0$Entry;

  inline$foo1$0$Entry:
    inline$foo1$0$x := x;
    goto inline$foo1$0$anon0;

  inline$foo1$0$anon0:
    x := x + 1;
    goto inline$foo2$0$Entry;

  inline$foo2$0$Entry:
    inline$foo2$0$x := x;
    goto inline$foo2$0$anon0;

  inline$foo2$0$anon0:
    x := x + 1;
    goto inline$foo3$1$Entry;

  inline$foo3$1$Entry:
    inline$foo3$1$x := x;
    goto inline$foo3$1$anon0;

  inline$foo3$1$anon0:
    x := x + 1;
    goto inline$foo1$1$Entry;

  inline$foo1$1$Entry:
    inline$foo1$1$x := x;
    goto inline$foo1$1$anon0;

  inline$foo1$1$anon0:
    x := x + 1;
    goto inline$foo2$1$Entry;

  inline$foo2$1$Entry:
    inline$foo2$1$x := x;
    goto inline$foo2$1$anon0;

  inline$foo2$1$anon0:
    x := x + 1;
    call foo3();
    goto inline$foo2$1$Return;

  inline$foo2$1$Return:
    goto inline$foo1$1$anon0$1;

  inline$foo1$1$anon0$1:
    goto inline$foo1$1$Return;

  inline$foo1$1$Return:
    goto inline$foo3$1$anon0$1;

  inline$foo3$1$anon0$1:
    goto inline$foo3$1$Return;

  inline$foo3$1$Return:
    goto inline$foo2$0$anon0$1;

  inline$foo2$0$anon0$1:
    goto inline$foo2$0$Return;

  inline$foo2$0$Return:
    goto inline$foo1$0$anon0$1;

  inline$foo1$0$anon0$1:
    goto inline$foo1$0$Return;

  inline$foo1$0$Return:
    goto inline$foo3$0$anon0$1;

  inline$foo3$0$anon0$1:
    goto inline$foo3$0$Return;

  inline$foo3$0$Return:
    goto anon0$1;

  anon0$1:
    return;
}


after inlining procedure calls
procedure {:inline 2} foo3();
  modifies x;


implementation {:inline 2} foo3()
{
  var inline$foo1$0$x: int;
  var inline$foo2$0$x: int;
  var inline$foo3$0$x: int;
  var inline$foo1$1$x: int;
  var inline$foo2$1$x: int;
  var inline$foo3$1$x: int;

  anon0:
    x := x + 1;
    goto inline$foo1$0$Entry;

  inline$foo1$0$Entry:
    inline$foo1$0$x := x;
    goto inline$foo1$0$anon0;

  inline$foo1$0$anon0:
    x := x + 1;
    goto inline$foo2$0$Entry;

  inline$foo2$0$Entry:
    inline$foo2$0$x := x;
    goto inline$foo2$0$anon0;

  inline$foo2$0$anon0:
    x := x + 1;
    goto inline$foo3$0$Entry;

  inline$foo3$0$Entry:
    inline$foo3$0$x := x;
    goto inline$foo3$0$anon0;

  inline$foo3$0$anon0:
    x := x + 1;
    goto inline$foo1$1$Entry;

  inline$foo1$1$Entry:
    inline$foo1$1$x := x;
    goto inline$foo1$1$anon0;

  inline$foo1$1$anon0:
    x := x + 1;
    goto inline$foo2$1$Entry;

  inline$foo2$1$Entry:
    inline$foo2$1$x := x;
    goto inline$foo2$1$anon0;

  inline$foo2$1$anon0:
    x := x + 1;
    goto inline$foo3$1$Entry;

  inline$foo3$1$Entry:
    inline$foo3$1$x := x;
    goto inline$foo3$1$anon0;

  inline$foo3$1$anon0:
    x := x + 1;
    call foo1();
    goto inline$foo3$1$Return;

  inline$foo3$1$Return:
    goto inline$foo2$1$anon0$1;

  inline$foo2$1$anon0$1:
    goto inline$foo2$1$Return;

  inline$foo2$1$Return:
    goto inline$foo1$1$anon0$1;

  inline$foo1$1$anon0$1:
    goto inline$foo1$1$Return;

  inline$foo1$1$Return:
    goto inline$foo3$0$anon0$1;

  inline$foo3$0$anon0$1:
    goto inline$foo3$0$Return;

  inline$foo3$0$Return:
    goto inline$foo2$0$anon0$1;

  inline$foo2$0$anon0$1:
    goto inline$foo2$0$Return;

  inline$foo2$0$Return:
    goto inline$foo1$0$anon0$1;

  inline$foo1$0$anon0$1:
    goto inline$foo1$0$Return;

  inline$foo1$0$Return:
    goto anon0$1;

  anon0$1:
    return;
}


after inlining procedure calls
procedure bar();
  modifies x;


implementation bar()
{
  var inline$foo$0$x: int;
  var inline$foo$1$x: int;
  var inline$foo1$0$x: int;
  var inline$foo2$0$x: int;
  var inline$foo3$0$x: int;
  var inline$foo1$1$x: int;
  var inline$foo2$1$x: int;
  var inline$foo3$1$x: int;

  anon0:
    goto inline$foo$0$Entry;

  inline$foo$0$Entry:
    inline$foo$0$x := x;
    goto inline$foo$0$anon0;

  inline$foo$0$anon0:
    x := x + 1;
    goto inline$foo$1$Entry;

  inline$foo$1$Entry:
    inline$foo$1$x := x;
    goto inline$foo$1$anon0;

  inline$foo$1$anon0:
    x := x + 1;
    call foo();
    goto inline$foo$1$Return;

  inline$foo$1$Return:
    goto inline$foo$0$anon0$1;

  inline$foo$0$anon0$1:
    goto inline$foo$0$Return;

  inline$foo$0$Return:
    goto anon0$1;

  anon0$1:
    goto inline$foo1$0$Entry;

  inline$foo1$0$Entry:
    inline$foo1$0$x := x;
    goto inline$foo1$0$anon0;

  inline$foo1$0$anon0:
    x := x + 1;
    goto inline$foo2$0$Entry;

  inline$foo2$0$Entry:
    inline$foo2$0$x := x;
    goto inline$foo2$0$anon0;

  inline$foo2$0$anon0:
    x := x + 1;
    goto inline$foo3$0$Entry;

  inline$foo3$0$Entry:
    inline$foo3$0$x := x;
    goto inline$foo3$0$anon0;

  inline$foo3$0$anon0:
    x := x + 1;
    goto inline$foo1$1$Entry;

  inline$foo1$1$Entry:
    inline$foo1$1$x := x;
    goto inline$foo1$1$anon0;

  inline$foo1$1$anon0:
    x := x + 1;
    goto inline$foo2$1$Entry;

  inline$foo2$1$Entry:
    inline$foo2$1$x := x;
    goto inline$foo2$1$anon0;

  inline$foo2$1$anon0:
    x := x + 1;
    goto inline$foo3$1$Entry;

  inline$foo3$1$Entry:
    inline$foo3$1$x := x;
    goto inline$foo3$1$anon0;

  inline$foo3$1$anon0:
    x := x + 1;
    call foo1();
    goto inline$foo3$1$Return;

  inline$foo3$1$Return:
    goto inline$foo2$1$anon0$1;

  inline$foo2$1$anon0$1:
    goto inline$foo2$1$Return;

  inline$foo2$1$Return:
    goto inline$foo1$1$anon0$1;

  inline$foo1$1$anon0$1:
    goto inline$foo1$1$Return;

  inline$foo1$1$Return:
    goto inline$foo3$0$anon0$1;

  inline$foo3$0$anon0$1:
    goto inline$foo3$0$Return;

  inline$foo3$0$Return:
    goto inline$foo2$0$anon0$1;

  inline$foo2$0$anon0$1:
    goto inline$foo2$0$Return;

  inline$foo2$0$Return:
    goto inline$foo1$0$anon0$1;

  inline$foo1$0$anon0$1:
    goto inline$foo1$0$Return;

  inline$foo1$0$Return:
    goto anon0$2;

  anon0$2:
    return;
}



Boogie program verifier finished with 5 verified, 0 errors
-------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
    test5.bpl(34,10): anon0
    test5.bpl(28,10): inline$P$0$anon0
    test5.bpl(28,10): inline$P$1$anon0
    test5.bpl(34,10): anon0$2

Boogie program verifier finished with 4 verified, 1 error
-------------------- expansion3.bpl --------------------
*** detected expansion loop on foo3
*** detected expansion loop on foo3
*** detected expansion loop on foo3

Boogie program verifier finished with 1 verified, 0 errors
-------------------- expansion4.bpl --------------------

Boogie program verifier finished with 1 verified, 0 errors
-------------------- Elevator.bpl --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    Elevator.bpl(15,3): anon0
    Elevator.bpl(15,3): anon0$1
    Elevator.bpl(16,3): anon10_LoopHead
    Elevator.bpl(19,5): anon10_LoopBody
    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
    Elevator.bpl(24,7): anon13_Then$1

Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl with empty blocks --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    Elevator.bpl(15,3): anon0
    Elevator.bpl(68,23): inline$Initialize$0$Entry
    Elevator.bpl(71,13): inline$Initialize$0$anon0
    Elevator.bpl(68,23): inline$Initialize$0$Return
    Elevator.bpl(15,3): anon0$1
    Elevator.bpl(16,3): anon10_LoopHead
    Elevator.bpl(19,5): anon10_LoopBody
    Elevator.bpl(19,5): anon11_Else
    Elevator.bpl(19,5): anon12_Else
    Elevator.bpl(24,7): anon13_Then
    Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
    Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
    Elevator.bpl(24,7): anon13_Then$1

Boogie program verifier finished with 1 verified, 1 error
-------------------- expansion2.bpl --------------------

Boogie program verifier finished with 1 verified, 0 errors

---------- EXPANSION2.SX: 0

---------- EXPANSION2.SX: 0
-------------------- fundef.bpl --------------------

function {:inline true} foo(x: int) : bool
{
  x > 0
}

function {:inline false} foo2(x: int) : bool;

// autogenerated definition axiom
axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));

function foo3(x: int) : bool;

// autogenerated definition axiom
axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

Boogie program verifier finished with 0 verified, 0 errors
fundef2.bpl(6,3): Error BP5001: This assertion might not hold.
Execution trace:
    fundef2.bpl(5,3): anon0

Boogie program verifier finished with 0 verified, 1 error
-------------------- polyInline.bpl --------------------
polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
    polyInline.bpl(20,3): anon0
polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
    polyInline.bpl(27,3): anon0

Boogie program verifier finished with 0 verified, 2 errors
polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
    polyInline.bpl(20,3): anon0
polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
    polyInline.bpl(27,3): anon0

Boogie program verifier finished with 0 verified, 2 errors