Removed old test infrastructure files except for

./AbsHoudini/
./doomed/
./z3api/
./test17/

because their conversion to lit incomplete.

2 files changed, 0 insertions, 1613 deletions

diff --git a/Test/inline/Answer b/Test/inline/Answer
deleted file mode 100644
index 88e3ed5f..00000000
--- a/Test/inline/Answer
+++ /dev/null
@@ -1,1570 +0,0 @@
--------------------- test0.bpl --------------------

-test0.bpl(32,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    test0.bpl(28,3): anon0

-    test0.bpl(32,5): anon3_Then

-

-Boogie program verifier finished with 1 verified, 1 error

--------------------- codeexpr.bpl --------------------

-codeexpr.bpl(42,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    codeexpr.bpl(41,7): anon0

-

-Boogie program verifier finished with 5 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;

-    havoc inline$inc$0$y;

-    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;

-    havoc inline$incdec$0$z;

-    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;

-    havoc inline$dec$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;

-    havoc inline$dec$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;

-    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;

-    havoc inline$increase$0$j, inline$increase$0$k;

-    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;

-    havoc inline$recursive$0$k, inline$recursive$0$y;

-    goto inline$recursive$0$anon0;

-

-  inline$recursive$0$anon0:

-    goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

-

-  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;

-    havoc inline$recursive$1$k, inline$recursive$1$y;

-    goto inline$recursive$1$anon0;

-

-  inline$recursive$1$anon0:

-    goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

-

-  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;

-    havoc inline$recursive$2$k, inline$recursive$2$y;

-    goto inline$recursive$2$anon0;

-

-  inline$recursive$2$anon0:

-    goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

-

-  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$anon3_Then:

-    assume {:partition} inline$recursive$2$x == 0;

-    inline$recursive$2$y := 1;

-    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$anon3_Then:

-    assume {:partition} inline$recursive$1$x == 0;

-    inline$recursive$1$y := 1;

-    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$anon3_Then:

-    assume {:partition} inline$recursive$0$x == 0;

-    inline$recursive$0$y := 1;

-    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_Else:

-    assume {:partition} x != 0;

-    goto inline$recursive$0$Entry;

-

-  inline$recursive$0$Entry:

-    inline$recursive$0$x := x - 1;

-    havoc inline$recursive$0$k, inline$recursive$0$y;

-    goto inline$recursive$0$anon0;

-

-  inline$recursive$0$anon0:

-    goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

-

-  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;

-    havoc inline$recursive$1$k, inline$recursive$1$y;

-    goto inline$recursive$1$anon0;

-

-  inline$recursive$1$anon0:

-    goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

-

-  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;

-    havoc inline$recursive$2$k, inline$recursive$2$y;

-    goto inline$recursive$2$anon0;

-

-  inline$recursive$2$anon0:

-    goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

-

-  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$anon3_Then:

-    assume {:partition} inline$recursive$2$x == 0;

-    inline$recursive$2$y := 1;

-    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$anon3_Then:

-    assume {:partition} inline$recursive$1$x == 0;

-    inline$recursive$1$y := 1;

-    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$anon3_Then:

-    assume {:partition} inline$recursive$0$x == 0;

-    inline$recursive$0$y := 1;

-    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;

-

-  anon3_Then:

-    assume {:partition} x == 0;

-    y := 1;

-    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 := -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;

-    havoc inline$find$0$i, inline$find$0$b, inline$find$0$ret, inline$find$0$found;

-    goto inline$find$0$anon0;

-

-  inline$find$0$anon0:

-    inline$find$0$ret := -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;

-    havoc inline$check$0$ret;

-    goto inline$check$0$anon0;

-

-  inline$check$0$anon0:

-    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

-

-  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$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$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_Else:

-    assume {:partition} !inline$find$0$b;

-    goto inline$find$0$anon4_LoopHead;

-

-  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$anon3:

-    goto inline$find$0$Return;

-

-  inline$find$0$anon4_LoopDone:

-    assume {:partition} inline$find$0$size <= inline$find$0$i;

-    goto inline$find$0$anon3;

-

-  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_Else:

-    assume {:partition} !b;

-    goto anon2;

-

-  anon2:

-    return;

-

-  anon3_Then:

-    assume {:partition} b;

-    assert i > 0 && A[i] == x;

-    goto anon2;

-}

-

-

-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 := -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;

-    havoc inline$check$0$ret;

-    goto inline$check$0$anon0;

-

-  inline$check$0$anon0:

-    goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

-

-  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$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$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_Else:

-    assume {:partition} !b;

-    goto anon4_LoopHead;

-

-  anon5_Then:

-    assume {:partition} b;

-    ret := i;

-    found := b;

-    goto anon3;

-

-  anon3:

-    return;

-

-  anon4_LoopDone:

-    assume {:partition} size <= i;

-    goto anon3;

-}

-

-

-<console>(70,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>(29,0): inline$find$0$anon0

-    <console>(39,0): inline$find$0$anon4_LoopBody

-    <console>(43,0): inline$check$0$Entry

-    <console>(54,0): inline$check$0$anon4_Else

-    <console>(67,0): inline$check$0$Return

-<console>(109,4): Error BP5001: This assertion might not hold.

-Execution trace:

-    <console>(19,0): anon0

-    <console>(29,0): inline$find$0$anon0

-    <console>(39,0): inline$find$0$anon4_LoopBody

-    <console>(43,0): inline$check$0$Entry

-    <console>(62,0): inline$check$0$anon4_Then

-    <console>(67,0): inline$check$0$Return

-    <console>(79,0): inline$find$0$anon5_Then

-    <console>(107,0): anon3_Then

-<console>(51,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>(35,0): inline$check$0$anon4_Else

-    <console>(48,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(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    test5.bpl(36,10): anon0

-    test5.bpl(30,10): inline$P$0$anon0

-    test5.bpl(30,10): inline$P$1$anon0

-    test5.bpl(36,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(20,5): Error BP5005: This loop invariant might not be maintained by the loop.

-Execution trace:

-    Elevator.bpl(18,3): anon0

-    Elevator.bpl(18,3): anon0$1

-    Elevator.bpl(19,3): anon10_LoopHead

-    Elevator.bpl(22,5): anon10_LoopBody

-    Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0

-    Elevator.bpl(27,7): anon13_Then$1

-

-Boogie program verifier finished with 1 verified, 1 error

--------------------- Elevator.bpl with empty blocks --------------------

-Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.

-Execution trace:

-    Elevator.bpl(18,3): anon0

-    Elevator.bpl(71,23): inline$Initialize$0$Entry

-    Elevator.bpl(74,13): inline$Initialize$0$anon0

-    Elevator.bpl(71,23): inline$Initialize$0$Return

-    Elevator.bpl(18,3): anon0$1

-    Elevator.bpl(19,3): anon10_LoopHead

-    Elevator.bpl(22,5): anon10_LoopBody

-    Elevator.bpl(22,5): anon11_Else

-    Elevator.bpl(22,5): anon12_Else

-    Elevator.bpl(27,7): anon13_Then

-    Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry

-    Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0

-    Elevator.bpl(97,23): inline$MoveDown_Error$0$Return

-    Elevator.bpl(27,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;

-

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

-

-function foo3(x: int) : bool;

-

-axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

-

-Boogie program verifier finished with 0 verified, 0 errors

-fundef2.bpl(8,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    fundef2.bpl(7,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

--------------------- polyInline.bpl --------------------

-polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(26,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    polyInline.bpl(23,3): anon0

-polyInline.bpl(42,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    polyInline.bpl(30,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

-polyInline.bpl(30,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(34,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(38,9): Warning: type parameter alpha is ambiguous, instantiating to int

-polyInline.bpl(26,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    polyInline.bpl(23,3): anon0

-polyInline.bpl(42,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    polyInline.bpl(30,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

--------------------- InliningAndLoops.bpl --------------------

-InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    InliningAndLoops.bpl(7,10): anon0#3

-    InliningAndLoops.bpl(8,3): anon4_LoopHead#3

-    InliningAndLoops.bpl(10,5): anon4_LoopBody#3

-    InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3

-    InliningAndLoops.bpl(8,3): anon4_LoopHead#2

-    InliningAndLoops.bpl(10,5): anon4_LoopBody#2

-    InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2

-    InliningAndLoops.bpl(8,3): anon4_LoopHead#1

-    InliningAndLoops.bpl(8,3): anon4_LoopDone#3

-    InliningAndLoops.bpl(14,5): anon5_Then#3

-

-Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
deleted file mode 100644
index f025de1b..00000000
--- a/Test/inline/runtest.bat
+++ /dev/null
@@ -1,43 +0,0 @@
-@echo off

-setlocal

-

-set BGEXE=..\..\Binaries\Boogie.exe

-

-for %%f in (test0.bpl codeexpr.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% %* %%f

-)

-

-for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f

-)

-

-for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% %* %%f

-)

-

-REM Peephole optimizations are so good that Elevator seems worthwhile

-REM to include twice among these inline tests

-for %%f in (Elevator.bpl) do (

-  echo -------------------- %%f with empty blocks --------------------

-  %BGEXE% /removeEmptyBlocks:0 %* %%f

-)

-

-echo -------------------- expansion2.bpl --------------------

-%BGEXE% %* /proverLog:expansion2.sx expansion2.bpl

-%SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx

-%SystemRoot%\system32\find.exe /C "xxf1" expansion2.sx

-

-echo -------------------- fundef.bpl --------------------

-%BGEXE% %* /print:- /env:0 fundef.bpl

-%BGEXE% %* fundef2.bpl

-

-echo -------------------- polyInline.bpl --------------------

-%BGEXE% %* /typeEncoding:predicates /logPrefix:p polyInline.bpl

-%BGEXE% %* /typeEncoding:arguments /logPrefix:a polyInline.bpl

-

-echo -------------------- InliningAndLoops.bpl --------------------

-%BGEXE% %* /loopUnroll:3 /soundLoopUnrolling InliningAndLoops.bpl

-