Removed Output files. These are created on a local machine when the tests are run.

19 files changed, 0 insertions, 4745 deletions

diff --git a/Test/aitest0/Output b/Test/aitest0/Output
deleted file mode 100644
index 58750460..00000000
--- a/Test/aitest0/Output
+++ /dev/null
@@ -1,111 +0,0 @@
-var GlobalFlag: bool;

-

-const A: int;

-

-const B: int;

-

-const C: int;

-

-procedure Join(b: bool);

-  modifies GlobalFlag;

-

-

-

-implementation Join(b: bool)

-{

-  var x: int;

-  var y: int;

-  var z: int;

-

-  start:

-    assume true;

-    GlobalFlag := true;

-    x := 3;

-    y := 4;

-    z := x + y;

-    assume x == 3 && y == 4 && z == 7;

-    goto Then, Else;

-

-  Then:

-    assume x == 3 && y == 4 && z == 7;

-    assume b <==> true;

-    x := x + 1;

-    assume x == 4 && y == 4 && z == 7;

-    goto join;

-

-  Else:

-    assume x == 3 && y == 4 && z == 7;

-    assume b <==> false;

-    y := 4;

-    assume x == 3 && y == 4 && z == 7;

-    goto join;

-

-  join:

-    assume y == 4 && z == 7;

-    assert y == 4;

-    assert z == 7;

-    assert GlobalFlag <==> true;

-    assume y == 4 && z == 7;

-    return;

-}

-

-

-

-procedure Loop();

-

-

-

-implementation Loop()

-{

-  var c: int;

-  var i: int;

-

-  start:

-    assume true;

-    c := 0;

-    i := 0;

-    assume c == 0 && i == 0;

-    goto test;

-

-  test:  // cut point

-    assume c == 0;

-    assume c == 0;

-    goto Then, Else;

-

-  Then:

-    assume c == 0;

-    assume i < 10;

-    i := i + 1;

-    assume c == 0;

-    goto test;

-

-  Else:

-    assume c == 0;

-    assume c == 0;

-    return;

-}

-

-

-

-procedure Evaluate();

-

-

-

-implementation Evaluate()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 5;

-    i := 3 * i + 1;

-    i := 3 * (i + 1);

-    i := 1 + 3 * i;

-    i := (i + 1) * 3;

-    assume i == 465;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

diff --git a/Test/aitest1/Output b/Test/aitest1/Output
deleted file mode 100644
index 4e5c8f27..00000000
--- a/Test/aitest1/Output
+++ /dev/null
@@ -1,510 +0,0 @@
--------------------- ineq.bpl --------------------

-procedure SimpleLoop();

-

-

-

-implementation SimpleLoop()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 0;

-    assume i == 0;

-    goto test;

-

-  test:  // cut point

-    assume 0 <= i;

-    assume 0 <= i;

-    goto Then, Else;

-

-  Then:

-    assume 0 <= i;

-    assume i < 10;

-    i := i + 1;

-    assume i <= 10 && 1 <= i;

-    goto test;

-

-  Else:

-    assume 0 <= i;

-    assume !(i < 10);

-    assume 10 <= i;

-    return;

-}

-

-

-

-procedure VariableBoundLoop(n: int);

-

-

-

-implementation VariableBoundLoop(n: int)

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 0;

-    assume i == 0;

-    goto test;

-

-  test:  // cut point

-    assume 0 <= i;

-    assume 0 <= i;

-    goto Then, Else;

-

-  Then:

-    assume 0 <= i;

-    assume i < n;

-    i := i + 1;

-    assume i <= n && 1 <= i;

-    goto test;

-

-  Else:

-    assume 0 <= i;

-    assume !(i < n);

-    assume n <= i && 0 <= i;

-    return;

-}

-

-

-

-procedure Foo();

-

-

-

-implementation Foo()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 3 * i + 1;

-    i := 3 * (i + 1);

-    i := 1 + 3 * i;

-    i := (i + 1) * 3;

-    assume true;

-    return;

-}

-

-

-

-procedure FooToo();

-

-

-

-implementation FooToo()

-{

-  var i: int;

-

-  start:

-    assume true;

-    i := 5;

-    i := 3 * i + 1;

-    i := 3 * (i + 1);

-    i := 1 + 3 * i;

-    i := (i + 1) * 3;

-    assume 1 / 3 * i == 155;

-    return;

-}

-

-

-

-procedure FooTooStepByStep();

-

-

-

-implementation FooTooStepByStep()

-{

-  var i: int;

-

-  L0:

-    assume true;

-    i := 5;

-    assume i == 5;

-    goto L1;

-

-  L1:

-    assume i == 5;

-    i := 3 * i + 1;

-    assume i == 16;

-    goto L2;

-

-  L2:

-    assume i == 16;

-    i := 3 * (i + 1);

-    assume 1 / 3 * i == 17;

-    goto L3;

-

-  L3:

-    assume 1 / 3 * i == 17;

-    i := 1 + 3 * i;

-    assume i == 154;

-    goto L4;

-

-  L4:

-    assume i == 154;

-    i := (i + 1) * 3;

-    assume 1 / 3 * i == 155;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear0.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear1.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume x * x == y;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear2.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume x == 8;

-    assume x == 8;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear3.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  start:

-    assume true;

-    assume x < y;

-    assume x + 1 <= y;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear4.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-  modifies x;

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    assume x < y;

-    assume x + 1 <= y;

-    goto B;

-

-  B:

-    assume x + 1 <= y;

-    x := x * x;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear5.bpl --------------------

-var x: int;

-

-var y: int;

-

-procedure p();

-  modifies x;

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    assume 0 - 1 <= x;

-    assume -1 <= x;

-    goto B;

-

-  B:

-    assume -1 <= x;

-    assume x < y;

-    assume x + 1 <= y && -1 <= x;

-    goto C;

-

-  C:

-    assume x + 1 <= y && -1 <= x;

-    x := x * x;

-    assume 0 <= y;

-    goto D;

-

-  D:

-    assume 0 <= y;

-    x := y;

-    assume x == y && 0 <= y;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear6.bpl --------------------

-var x: int;

-

-var y: int;

-

-var z: int;

-

-procedure p();

-  modifies x;

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    x := 8;

-    assume x == 8;

-    goto B, C;

-

-  B:

-    assume x == 8;

-    x := 9;

-    assume x == 9;

-    goto D;

-

-  C:

-    assume x == 8;

-    x := 10;

-    assume x == 10;

-    goto D;

-

-  D:

-    assume 9 <= x && x <= 10;

-    assume 9 <= x && x <= 10;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear7.bpl --------------------

-var x: int;

-

-var y: int;

-

-var z: int;

-

-procedure p();

-

-

-

-implementation p()

-{

-

-  A:

-    assume true;

-    assume true;

-    goto B, C;

-

-  B:

-    assume true;

-    assume x <= 0;

-    assume x <= 0;

-    goto D;

-

-  C:

-    assume true;

-    assume y <= 0;

-    assume y <= 0;

-    goto D;

-

-  D:

-    assume true;

-    assume true;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear8.bpl --------------------

-procedure foo();

-

-

-

-implementation foo()

-{

-  var i: int;

-  var j: int;

-  var n: int;

-

-  A:

-    assume true;

-    n := 0;

-    assume n == 0;

-    goto B;

-

-  B:

-    assume n == 0;

-    j := 0;

-    assume j == 0 && n == 0;

-    goto C;

-

-  C:

-    assume j == 0 && n == 0;

-    i := j + 1;

-    assume i == j + 1 && j == 0 && n == 0;

-    goto D;

-

-  D:

-    assume i == j + 1 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 2 && j == 0 && n == 0;

-    goto E;

-

-  E:

-    assume i == j + 2 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 3 && j == 0 && n == 0;

-    goto F;

-

-  F:

-    assume i == j + 3 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 4 && j == 0 && n == 0;

-    goto G;

-

-  G:

-    assume i == j + 4 && j == 0 && n == 0;

-    i := i + 1;

-    assume i == j + 5 && j == 0 && n == 0;

-    goto H;

-

-  H:

-    assume i == j + 5 && j == 0 && n == 0;

-    j := j + 1;

-    assume i == j + 4 && j == 1 && n == 0;

-    goto I;

-

-  I:

-    assume i == j + 4 && j == 1 && n == 0;

-    assume i == j + 4 && j == 1 && n == 0;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Linear9.bpl --------------------

-procedure foo();

-

-

-

-implementation foo()

-{

-  var i: int;

-  var j: int;

-  var n: int;

-

-  entry:

-    assume true;

-    assume n >= 4;

-    i := 0;

-    j := i + 1;

-    assume j == i + 1 && i == 0 && 4 <= n;

-    goto exit, loop0;

-

-  loop0:  // cut point

-    assume 4 <= n && 0 <= i && j == i + 1;

-    assume j <= n;

-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;

-    goto loop1;

-

-  loop1:

-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;

-    i := i + 1;

-    assume 1 <= i && j == i && j <= n && 4 <= n;

-    goto loop2;

-

-  loop2:

-    assume j <= n && 4 <= n && 1 <= i && j == i;

-    j := j + 1;

-    assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;

-    goto loop0, exit;

-

-  exit:

-    assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;

-    assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

--------------------- Bound.bpl -------------------- 

-

-Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/aitest9/Output b/Test/aitest9/Output
deleted file mode 100644
index dd10a8b3..00000000
--- a/Test/aitest9/Output
+++ /dev/null
@@ -1,26 +0,0 @@
- 

--------------------- VarMapFixPoint.bpl -------------------- 

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

-Execution trace:

-    VarMapFixPoint.bpl(5,3): start

-    VarMapFixPoint.bpl(10,3): LoopHead

-    VarMapFixPoint.bpl(14,3): LoopBody

-

-Boogie program verifier finished with 1 verified, 1 error

- 

--------------------- TestIntervals.bpl -------------------- 

-TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    TestIntervals.bpl(5,5): anon0

-    TestIntervals.bpl(6,3): anon9_LoopHead

-    TestIntervals.bpl(6,3): anon9_LoopDone

-    TestIntervals.bpl(11,5): anon2

-    TestIntervals.bpl(12,14): anon10_Then

-    TestIntervals.bpl(13,3): anon4

-    TestIntervals.bpl(13,14): anon11_Then

-    TestIntervals.bpl(14,3): anon6

-    TestIntervals.bpl(14,14): anon12_Then

-    TestIntervals.bpl(17,5): anon8

-    TestIntervals.bpl(21,3): Next

-

-Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/bitvectors/Output b/Test/bitvectors/Output
deleted file mode 100644
index 9ad91f5b..00000000
--- a/Test/bitvectors/Output
+++ /dev/null
@@ -1,62 +0,0 @@
--------------------- arrays.bpl --------------------

-

-Boogie program verifier finished with 2 verified, 0 errors

--------------------- bv0.bpl --------------------

-bv0.bpl(4,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32)

-bv0.bpl(5,3): Error: mismatched types in assignment command (cannot assign int to bv32)

-bv0.bpl(6,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)

-bv0.bpl(7,10): Error: start index in extract must be no bigger than the end index

-bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)

-bv0.bpl(9,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)

-bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32)

-7 type checking errors detected in bv0.bpl

--------------------- bv1.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- bv2.bpl --------------------

-bv2.bpl(4,13): Error: bitvector bounds in illegal position

-bv2.bpl(6,13): Error: undeclared type: x

-bv2.bpl(7,14): Error: bitvector bounds in illegal position

-3 name resolution errors detected in bv2.bpl

--------------------- bv3.bpl --------------------

-bv3.bpl(2,5): Error: type name: bv16 is registered for bitvectors

-1 name resolution errors detected in bv3.bpl

--------------------- bv4.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- bv7.bpl --------------------

-bv7.bpl(4,14): Error: arguments of extract need to be integer literals

-bv7.bpl(5,15): Error: parentheses around bitvector bounds are not allowed

-2 parse errors detected in bv7.bpl

--------------------- vcc0.bpl --------------------

-vcc0.bpl(553,22): syntax error: [ expected

-vcc0.bpl(553,28): syntax error: ] expected

-vcc0.bpl(555,29): syntax error: [ expected

-vcc0.bpl(557,28): syntax error: [ expected

-vcc0.bpl(557,37): syntax error: ] expected

-5 parse errors detected in vcc0.bpl

--------------------- vcc0.bpl - toInt --------------------

-vcc0.bpl(553,22): syntax error: [ expected

-vcc0.bpl(553,28): syntax error: ] expected

-vcc0.bpl(555,29): syntax error: [ expected

-vcc0.bpl(557,28): syntax error: [ expected

-vcc0.bpl(557,37): syntax error: ] expected

-5 parse errors detected in vcc0.bpl

--------------------- bv4.bpl - /bv:n --------------------

-bv4.bpl(3,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-bv4.bpl(3,13): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-bv4.bpl(5,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-4 type checking errors detected in bv4.bpl

--------------------- bv5.bpl --------------------

-bv5.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    bv5.bpl(5,12): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

--------------------- bv6.bpl --------------------

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

-Execution trace:

-    bv6.bpl(5,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/dafny0/Output b/Test/dafny0/Output
deleted file mode 100644
index 64c43c87..00000000
--- a/Test/dafny0/Output
+++ /dev/null
@@ -1,100 +0,0 @@
-

--------------------- Simple.dfy --------------------

-// synthetic program

-

-class MyClass<T, U> {

-  var x: int;

-

-  method M(s: bool, lotsaObjects: set<object>)

-      returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>):

-    requires s;

-    modifies this;

-    modifies lotsaObjects;

-    ensures t == t;

-    ensures old(null) != this;

-  {

-    x := 12;

-    while (x < 100)

-      invariant x <= 100;

-    {

-      x := x + 17;

-      if (x % 20 == 3) {

-        x := this.x + 1;

-      } else {

-        this.x := x + 0;

-      }

-      call t, u, v := M(true, lotsaObjects)

-      var to: MyClass<T,U>;

-      call to, u, v := M(true, lotsaObjects)

-      call to, u, v := to.M(true, lotsaObjects)

-    }

-  }

-}

-

-Dafny program verifier finished with 0 verified, 0 errors

-

--------------------- BQueue.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

--------------------- SmallTests.dfy --------------------

-

-Dafny program verifier finished with 3 verified, 0 errors

-

--------------------- Queue.dfy --------------------

-

-Dafny program verifier finished with 12 verified, 0 errors

-

--------------------- ListCopy.dfy --------------------

-

-Dafny program verifier finished with 2 verified, 0 errors

-

--------------------- BinaryTree.dfy --------------------

-

-Dafny program verifier finished with 13 verified, 0 errors

-

--------------------- ListReverse.dfy --------------------

-

-Dafny program verifier finished with 1 verified, 0 errors

-

--------------------- ListContents.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- SchorrWaite.dfy --------------------

-

-Dafny program verifier finished with 4 verified, 0 errors

-

--------------------- Termination.dfy --------------------

-

-Dafny program verifier finished with 5 verified, 0 errors

-

--------------------- Use.dfy --------------------

-Use.dfy(12,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): anon0

-Use.dfy(25,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): anon0

-Use.dfy(50,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 6 verified, 3 errors

-

--------------------- DTypes.dfy --------------------

-DTypes.dfy(15,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(28,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(54,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 5 verified, 3 errors

-

--------------------- TypeParameters.dfy --------------------

-

-Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/havoc0/Output b/Test/havoc0/Output
deleted file mode 100644
index 80fd4aa3..00000000
--- a/Test/havoc0/Output
+++ /dev/null
@@ -1,12 +0,0 @@
-

-Boogie program verifier finished with 1 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/inline/Output b/Test/inline/Output
deleted file mode 100644
index 39d5a5b4..00000000
--- a/Test/inline/Output
+++ /dev/null
@@ -1,983 +0,0 @@
--------------------- 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 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 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 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 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 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 recursive(x: int) returns (y: int)

-{

-  var k: int;

-

-  anon0:

-    goto anon3_Then, anon3_Else;

-

-  anon3_Then:

-    assume x == 0;

-    y := 1;

-    return;

-

-  anon3_Else:

-    assume 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 inline$recursive$0$x == 0;

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

-    goto inline$recursive$0$Return;

-

-  inline$recursive$0$anon3_Else:

-    assume inline$recursive$0$x != 0;

-    goto inline$recursive$0$anon2;

-

-  inline$recursive$0$anon2:

-    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 inline$recursive$1$x == 0;

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

-    goto inline$recursive$1$Return;

-

-  inline$recursive$1$anon3_Else:

-    assume inline$recursive$1$x != 0;

-    goto inline$recursive$1$anon2;

-

-  inline$recursive$1$anon2:

-    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 inline$recursive$2$x == 0;

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

-    goto inline$recursive$2$Return;

-

-  inline$recursive$2$anon3_Else:

-    assume inline$recursive$2$x != 0;

-    goto inline$recursive$2$anon2;

-

-  inline$recursive$2$anon2:

-    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$anon2$1;

-

-  inline$recursive$1$anon2$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$anon2$1;

-

-  inline$recursive$0$anon2$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 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 x == 0;

-    y := 1;

-    return;

-

-  anon3_Else:

-    assume x != 0;

-    goto anon2;

-

-  anon2:

-    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 inline$recursive$0$x == 0;

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

-    goto inline$recursive$0$Return;

-

-  inline$recursive$0$anon3_Else:

-    assume inline$recursive$0$x != 0;

-    goto inline$recursive$0$anon2;

-

-  inline$recursive$0$anon2:

-    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 inline$recursive$1$x == 0;

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

-    goto inline$recursive$1$Return;

-

-  inline$recursive$1$anon3_Else:

-    assume inline$recursive$1$x != 0;

-    goto inline$recursive$1$anon2;

-

-  inline$recursive$1$anon2:

-    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 inline$recursive$2$x == 0;

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

-    goto inline$recursive$2$Return;

-

-  inline$recursive$2$anon3_Else:

-    assume inline$recursive$2$x != 0;

-    goto inline$recursive$2$anon2;

-

-  inline$recursive$2$anon2:

-    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$anon2$1;

-

-  inline$recursive$1$anon2$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$anon2$1;

-

-  inline$recursive$0$anon2$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 anon2$1;

-

-  anon2$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 b;

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

-    goto anon2;

-

-  anon3_Else:

-    assume !b;

-    goto anon2;

-

-  anon2:

-    return;

-}

-

-

-

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

-

-

-

-implementation 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 i < size;

-    call b := check(A, i, x);

-    goto anon5_Then, anon5_Else;

-

-  anon5_Then:

-    assume b;

-    ret := i;

-    found := b;

-    goto anon3;

-

-  anon5_Else:

-    assume !b;

-    goto anon4_LoopHead;

-

-  anon4_LoopDone:

-    assume i >= size;

-    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 check(A: [int]int, i: int, c: int) returns (ret: bool)

-{

-

-  anon0:

-    goto anon4_Then, anon4_Else;

-

-  anon4_Then:

-    assume A[i] == c;

-    ret := true;

-    goto anon3;

-

-  anon4_Else:

-    assume 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 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 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 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 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 !inline$find$0$b;

-    goto inline$find$0$anon4_LoopHead;

-

-  inline$find$0$anon4_LoopDone:

-    assume inline$find$0$i >= inline$find$0$size;

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

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

-    goto anon2;

-

-  anon3_Else:

-    assume !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 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 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 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 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 b;

-    ret := i;

-    found := b;

-    goto anon3;

-

-  anon5_Else:

-    assume !b;

-    goto anon4_LoopHead;

-

-  anon4_LoopDone:

-    assume i >= size;

-    goto anon3;

-

-  anon3:

-    return;

-}

-

-

-<console>(68,4): Error BP5003: A postcondition might not hold at this return statement.

-<console>(78,2): Related location: This is the postcondition that might not hold.

-Execution trace:

-    <console>(19,0): anon0

-    <console>(22,0): inline$find$0$Entry

-    <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>(22,0): inline$find$0$Entry

-    <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 at this return statement.

-<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 at this return statement.

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

--------------------- test5.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- test6.bpl --------------------

-test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo

-test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2

-test6.bpl(22,22): Error: the inlined procedure is recursive, call stack: foo3 -> foo1 -> foo2 -> foo3

-test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1

-test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo

-test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1

-6 type checking errors detected in test6.bpl

--------------------- expansion.bpl --------------------

-expansion.bpl(29,14): Error: invalid type for argument 0 in application of foo1: bool (expected: int)

-expansion.bpl(13,16): Error: expansion: {:inline ...} expects either true or false as the argument

-expansion.bpl(14,22): Error: expansion: identifier was not quantified over

-expansion.bpl(15,22): Error: expansion: identifier was not quantified over

-expansion.bpl(16,22): Error: expansion: more variables quantified over, than used in function

-expansion.bpl(18,21): Error: expansion: axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))

-expansion.bpl(19,53): Error: expansion: only identifiers supported as function arguments

-expansion.bpl(33,22): Error: expansion: an identifier was used more than once

-8 type checking errors detected in expansion.bpl

--------------------- expansion3.bpl --------------------

-*** detected expansion loop on foo3

-*** detected expansion loop on foo3

-*** detected expansion loop on foo3

-*** more than one possible expansion for x1

-expansion3.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    expansion3.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

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

--------------------- expansion4.bpl --------------------

-

-Boogie program verifier finished with 3 verified, 0 errors

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

-

-function {:inline true} foo(x: int) returns (bool)

-{

-  x > 0

-}

-

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

-

-// autogenerated definition axiom

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

-

-function foo3(x: int) returns (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

diff --git a/Test/lock/Output b/Test/lock/Output
deleted file mode 100644
index bcfc9f1c..00000000
--- a/Test/lock/Output
+++ /dev/null
@@ -1,8 +0,0 @@
-

-Boogie program verifier finished with 3 verified, 0 errors

-LockIncorrect.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LockIncorrect.bpl(9,1): start

-    LockIncorrect.bpl(14,1): LoopHead

-

-Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/smoke/Output b/Test/smoke/Output
deleted file mode 100644
index 4141bdb0..00000000
--- a/Test/smoke/Output
+++ /dev/null
@@ -1,25 +0,0 @@
--------------------- smoke0.bpl --------------------

-found unreachable code:

-implementation b(x: int)

-{

-  var y: int;

-  var y@0: int;

-

-

-  anon0:

-    assume true;

-    assume true;

-    goto anon3_Then;

-

-  anon3_Then:

-    assume true;

-    assume x < 0;

-    y := 1;

-    assume 1 <= y && y <= 1;

-    assert false;

-    return;

-}

-

-

-

-Boogie program verifier finished with 4 verified, 0 errors

diff --git a/Test/test0/Output b/Test/test0/Output
deleted file mode 100644
index e8ea231e..00000000
--- a/Test/test0/Output
+++ /dev/null
@@ -1,252 +0,0 @@
-

-Boogie program verifier finished with 0 verified, 0 errors

-

-Boogie program verifier finished with 0 verified, 0 errors

-Triggers0.bpl(14,31): Error: the 'nopats' quantifier attribute expects a string-literal parameter

-1 parse errors detected in Triggers0.bpl

-Triggers1.bpl(7,17): Error: boolean operators are not allowed in triggers

-Triggers1.bpl(11,21): Error: boolean operators are not allowed in triggers

-Triggers1.bpl(15,9): Error: boolean operators are not allowed in triggers

-Triggers1.bpl(19,10): Error: boolean operators are not allowed in triggers

-Triggers1.bpl(23,17): Error: boolean operators are not allowed in triggers

-Triggers1.bpl(27,17): Error: boolean operators are not allowed in triggers

-Triggers1.bpl(32,17): Error: equality is not allowed in triggers

-Triggers1.bpl(36,17): Error: arithmetic comparisons are not allowed in triggers

-Triggers1.bpl(45,10): Error: quantifiers are not allowed in triggers

-Triggers1.bpl(53,7): Error: trigger must mention all quantified variables, but does not mention: x

-Triggers1.bpl(61,7): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(62,7): Error: trigger must mention all quantified variables, but does not mention: x

-Triggers1.bpl(70,9): Error: a matching pattern must be more than just a variable by itself: x

-Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but does not mention: z

-Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x

-Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g

-Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(106,40): Error: trigger must mention all quantified variables, but does not mention: x

-Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z

-Triggers1.bpl(110,57): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: x

-Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1

-Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0

-23 name resolution errors detected in Triggers1.bpl

-const x: int;

-

-const y: int;

-

-const z: int;

-

-const P: bool;

-

-const Q: bool;

-

-const R: bool;

-

-axiom x * (y + z) == x + y * z;

-

-axiom x * y + z == (x + y) * z;

-

-axiom x * y * z == x * y * z;

-

-axiom x * y * z * x == x * y * z;

-

-axiom x / y / z == x / (y / z);

-

-axiom x / y / (z / x) == x / y / z;

-

-axiom x - y - z == x - (y - z);

-

-axiom x - y - (z - x) == x - y - z;

-

-axiom x + y - z - x + y == 0;

-

-axiom x + y - z - x + y == x + y - (z - (x + y));

-

-axiom P ==> Q ==> R <==> P ==> Q ==> R;

-

-axiom (P ==> Q) ==> R ==> P <==> (P ==> Q) ==> R;

-

-axiom P <==> Q <==> R;

-

-axiom P ==> Q <==> Q ==> R <==> R ==> P;

-

-axiom (P && Q) || (Q && R);

-

-axiom (P || Q) && (Q || R);

-

-axiom P || Q || Q || R;

-

-axiom P && Q && Q && R;

-

-function f(int) returns (int);

-

-axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200);

-

-Boogie program verifier finished with 0 verified, 0 errors

-

-Boogie program verifier finished with 0 verified, 0 errors

-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

-2 type checking errors detected in Arrays1.bpl

-Types0.bpl(6,18): Error: expected identifier before ':'

-1 parse errors detected in Types0.bpl

-Types1.bpl(6,11): Error: undeclared type: x

-Types1.bpl(7,18): Error: undeclared type: x

-2 name resolution errors detected in Types1.bpl

-WhereParsing.bpl(14,37): Error: where clause not allowed here

-WhereParsing.bpl(15,33): Error: where clause not allowed here

-2 parse errors detected in WhereParsing.bpl

-WhereParsing0.bpl(17,38): Error: where clause not allowed here

-WhereParsing0.bpl(18,38): Error: where clause not allowed here

-2 parse errors detected in WhereParsing0.bpl

-WhereParsing1.bpl(14,27): syntax error: ) expected

-1 parse errors detected in WhereParsing1.bpl

-WhereParsing2.bpl(1,14): syntax error: ; expected

-1 parse errors detected in WhereParsing2.bpl

-WhereResolution.bpl(28,38): Error: undeclared identifier: alpha

-WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state contexts

-2 name resolution errors detected in WhereResolution.bpl

-BadLabels0.bpl(4,2): Error: more than one declaration of block name: X

-BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y

-2 name resolution errors detected in BadLabels0.bpl

-BadLabels1.bpl(4,3): Error: Error: goto label 'X' is undefined or out of reach

-BadLabels1.bpl(5,3): Error: Error: goto label 'Y' is undefined or out of reach

-BadLabels1.bpl(10,3): Error: Error: goto label 'X' is undefined or out of reach

-BadLabels1.bpl(24,5): Error: Error: goto label 'K' is undefined or out of reach

-BadLabels1.bpl(30,5): Error: Error: goto label 'A' is undefined or out of reach

-BadLabels1.bpl(38,7): Error: Error: goto label 'M' is undefined or out of reach

-BadLabels1.bpl(41,3): Error: Error: goto label 'B' is undefined or out of reach

-BadLabels1.bpl(47,3): Error: Error: break statement is not inside a loop

-BadLabels1.bpl(49,5): Error: Error: break statement is not inside a loop

-BadLabels1.bpl(60,5): Error: Error: break label 'B' must designate an enclosing statement

-BadLabels1.bpl(63,5): Error: Error: break label 'A' must designate an enclosing statement

-BadLabels1.bpl(64,5): Error: Error: break label 'C' must designate an enclosing statement

-BadLabels1.bpl(65,8): Error: Error: break label 'F' must designate an enclosing statement

-13 parse errors detected in BadLabels1.bpl

-LineParse.bpl(1,0): Error: Malformed (#line num [filename]) pragma: #line

-LineParse.bpl(2,0): Error: Malformed (#line num [filename]) pragma: #line

-LineParse.bpl(1,0): Error: Unrecognized pragma: #dontknow what this is    No, I don't    well, it's an error is what it is

-LineParse.bpl(3,0): Error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }}  // error: A B C . txt(12,0)

-LineParse.bpl(6,2): syntax error: EOF expected

-5 parse errors detected in LineParse.bpl

-LineResolve.bpl(5,1): Error: undeclared identifier: a

-LineResolve.bpl(7,2): Error: undeclared identifier: b

-LineResolve.bpl(12,0): Error: undeclared identifier: c

-LineResolve.bpl(13,10): Error: undeclared identifier: d

-LineResolve.bpl(12,0): Error: undeclared identifier: e

-LineResolve.bpl(2,0): Error: undeclared identifier: f

-LineResolve.bpl(900,0): Error: undeclared identifier: g

-Abc.txt(11,3): Error: undeclared identifier: h

-Abc.txt(13,0): Error: undeclared identifier: i

-Abc.txt(99,0): Error: undeclared identifier: j

-c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k

-A B C . txt(12,0): Error: undeclared identifier: l

-12 name resolution errors detected in LineResolve.bpl

-AttributeParsingErr.bpl(1,33): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(3,33): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(5,52): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(7,37): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(9,31): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(11,29): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(13,13): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(15,18): Error: only attributes, not triggers, allowed here

-AttributeParsingErr.bpl(20,26): Error: only attributes, not triggers, allowed here

-9 parse errors detected in AttributeParsingErr.bpl

-

-type {:sourcefile "test.ssc"} T;

-

-function {:source "test.scc"} f(int) returns (int);

-

-const {:description "The largest integer value"} unique MAXINT: int;

-

-axiom {:naming "MyFavoriteAxiom"} (forall i: int :: { f(i) } f(i) == i + 1);

-

-var {:description "memory"} $Heap: [ref,name]any;

-

-var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref,name]any;

-

-procedure {:use_impl 1} foo(x: int) returns (n: int);

-

-

-

-implementation {:id 1} foo(x: int) returns (n: int)

-{

-  block1:

-    return;

-}

-

-

-

-implementation {:id 2} foo(x: int) returns (n: int)

-{

-  block1:

-    return;

-}

-

-

-

-type ref;

-

-type any;

-

-type name;

-

-Boogie program verifier finished with 0 verified, 0 errors

-AttributeResolution.bpl(1,18): Error: undeclared identifier: foo

-AttributeResolution.bpl(3,18): Error: undeclared identifier: bar

-AttributeResolution.bpl(7,15): Error: undeclared identifier: qux

-AttributeResolution.bpl(7,41): Error: undeclared identifier: ij

-AttributeResolution.bpl(13,21): Error: undeclared identifier: bzzt

-AttributeResolution.bpl(15,20): Error: undeclared identifier: blt

-AttributeResolution.bpl(5,20): Error: undeclared identifier: baz

-AttributeResolution.bpl(9,18): Error: undeclared identifier: mux

-AttributeResolution.bpl(11,29): Error: undeclared identifier: fux

-9 name resolution errors detected in AttributeResolution.bpl

-

-function \true() returns (bool);

-

-type \procedure;

-

-procedure \old(any: \procedure) returns (\var: \procedure);

-

-

-

-implementation \old(any: \procedure) returns (\var: \procedure)

-{

-  var \modifies: \procedure;

-

-    \modifies := any;

-    \var := \modifies;

-}

-

-

-

-procedure qux(a: \procedure);

-

-

-

-implementation qux(a: \procedure)

-{

-  var \var: \procedure;

-  var x: bool;

-

-    call \var := \old(a);

-    x := \true();

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

-

-Boogie program verifier finished with 0 verified, 0 errors

-MapsResolutionErrors.bpl(6,9): Error: type variable must occur in map arguments: b

-MapsResolutionErrors.bpl(20,10): Error: type variable must occur in procedure arguments: a

-2 name resolution errors detected in MapsResolutionErrors.bpl

-Orderings.bpl(12,20): Error: undeclared identifier: x

-Orderings.bpl(15,23): Error: c0 occurs more than once as parent

-Orderings.bpl(16,19): Error: constant cannot be its own parent

-Orderings.bpl(18,20): Error: the parent of a constant has to be a constant

-4 name resolution errors detected in Orderings.bpl

-BadQuantifier.bpl(3,15): syntax error: invalid QuantifierBody

-1 parse errors detected in BadQuantifier.bpl

-EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a

-EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a

-2 name resolution errors detected in EmptyCallArgs.bpl

diff --git a/Test/test1/Output b/Test/test1/Output
deleted file mode 100644
index b0f4aac3..00000000
--- a/Test/test1/Output
+++ /dev/null
@@ -1,137 +0,0 @@
-Frame0.bpl(10,11): Error: undeclared identifier: a

-Frame0.bpl(12,11): Error: undeclared identifier: b

-2 name resolution errors detected in Frame0.bpl

-Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

-Frame1.bpl(17,6): Error: command assigns to an immutable variable: a

-Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

-Frame1.bpl(23,4): Error: command assigns to an immutable variable: a

-Frame1.bpl(27,12): Error: command assigns to an immutable variable: hh

-Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

-Frame1.bpl(30,7): Error: command assigns to an immutable variable: hh

-Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

-Frame1.bpl(33,4): Error: command assigns to an immutable variable: hh

-Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

-Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

-Frame1.bpl(84,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x

-Frame1.bpl(89,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)

-16 type checking errors detected in Frame1.bpl

-

-Boogie program verifier finished with 0 verified, 0 errors

-Arrays.bpl(15,14): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(16,14): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(20,7): Error: wrong number of arguments in map assignment: 2 instead of 1

-Arrays.bpl(21,7): Error: wrong number of arguments in map assignment: 1 instead of 2

-Arrays.bpl(41,13): Error: invalid type for argument 0 in map select: bool (expected: int)

-Arrays.bpl(42,16): Error: invalid argument types (bool and int) to binary operator ==

-Arrays.bpl(43,13): Error: invalid type for argument 0 in map select: int (expected: bool)

-Arrays.bpl(43,15): Error: invalid type for argument 1 in map select: int (expected: ref)

-Arrays.bpl(44,15): Error: invalid type for argument 1 in map select: bool (expected: ref)

-Arrays.bpl(44,23): Error: invalid type for argument 0 in map select: ref (expected: bool)

-Arrays.bpl(45,13): Error: invalid type for argument 0 in map select: ref (expected: bool)

-Arrays.bpl(45,18): Error: invalid type for argument 1 in map select: int (expected: ref)

-Arrays.bpl(45,2): Error: preconditions must be of type bool

-Arrays.bpl(46,13): Error: invalid type for argument 0 in map select: int (expected: bool)

-Arrays.bpl(46,15): Error: invalid type for argument 1 in map select: int (expected: ref)

-Arrays.bpl(50,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-Arrays.bpl(51,6): Error: invalid type for argument 0 in map assignment: int (expected: bool)

-Arrays.bpl(51,8): Error: invalid type for argument 1 in map assignment: int (expected: ref)

-Arrays.bpl(51,5): Error: mismatched types in assignment command (cannot assign ref to int)

-Arrays.bpl(52,7): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-Arrays.bpl(52,5): Error: mismatched types in assignment command (cannot assign int to bool)

-Arrays.bpl(53,12): Error: invalid type for argument 1 in map assignment: bool (expected: ref)

-Arrays.bpl(113,11): Error: invalid type for argument 0 in map select: name (expected: [int,int]bool)

-Arrays.bpl(114,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to [[int,int]bool,[name]name]int)

-Arrays.bpl(115,4): Error: mismatched types in assignment command (cannot assign name to [int,int]bool)

-Arrays.bpl(116,5): Error: mismatched types in assignment command (cannot assign name to bool)

-Arrays.bpl(117,8): Error: invalid type for argument 1 in map assignment: name (expected: [name]name)

-Arrays.bpl(118,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [[int,int]bool,[name]name]int)

-Arrays.bpl(123,10): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(124,14): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(125,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-Arrays.bpl(126,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [int,int][name]int)

-Arrays.bpl(127,4): Error: mismatched types in assignment command (cannot assign [int,int][name]int to [int,int][int]int)

-Arrays.bpl(130,21): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(131,5): Error: wrong number of arguments in map assignment: 2 instead of 1

-Arrays.bpl(132,13): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(133,17): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(134,14): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(166,12): Error: invalid type for argument 0 in application of Sf: [int,int]bool (expected: any)

-Arrays.bpl(176,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to <a>[int,a]bool)

-Arrays.bpl(177,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [int,int]bool)

-Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to <a>[int,a]bool)

-Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [any,any]bool)

-Arrays.bpl(180,4): Error: mismatched types in assignment command (cannot assign [ref]bool to [any]bool)

-Arrays.bpl(191,18): Error: invalid type for argument 0 in map select: any (expected: int)

-Arrays.bpl(198,11): Error: invalid type for argument 0 in map assignment: any (expected: int)

-Arrays.bpl(214,24): Error: invalid type for argument 0 in call to IntMethod: int (expected: any)

-Arrays.bpl(214,9): Error: invalid type for out-parameter 0 in call to IntMethod: any (expected: int)

-Arrays.bpl(215,4): Error: mismatched types in assignment command (cannot assign int to any)

-Arrays.bpl(216,4): Error: mismatched types in assignment command (cannot assign any to int)

-Arrays.bpl(218,24): Error: invalid type for argument 0 in call to AnyMethod: any (expected: int)

-Arrays.bpl(218,9): Error: invalid type for out-parameter 0 in call to AnyMethod: int (expected: any)

-52 type checking errors detected in Arrays.bpl

-WhereTyping.bpl(25,34): Error: invalid argument types (double and int) to binary operator +

-WhereTyping.bpl(26,12): Error: where clauses must be of type bool

-WhereTyping.bpl(36,22): Error: invalid argument types (name and int) to binary operator !=

-WhereTyping.bpl(41,30): Error: invalid argument types (name and int) to binary operator ==

-4 type checking errors detected in WhereTyping.bpl

-Family.bpl(30,4): Error: mismatched types in assignment command (cannot assign int to bool)

-Family.bpl(31,8): Error: mismatched types in assignment command (cannot assign bool to int)

-Family.bpl(33,8): Error: mismatched types in assignment command (cannot assign int to y)

-Family.bpl(34,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

-Family.bpl(35,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

-Family.bpl(37,8): Error: mismatched types in assignment command (cannot assign bool to any)

-Family.bpl(38,8): Error: mismatched types in assignment command (cannot assign Field any to any)

-Family.bpl(39,8): Error: mismatched types in assignment command (cannot assign Field y to any)

-8 type checking errors detected in Family.bpl

-AttributeTyping.bpl(3,23): Error: ++ operands need to be bitvectors (got int, int)

-AttributeTyping.bpl(5,29): Error: invalid type for argument 0 in application of F0: bool (expected: int)

-AttributeTyping.bpl(7,26): Error: invalid type for argument 0 in application of F0: bool (expected: int)

-AttributeTyping.bpl(9,21): Error: invalid argument types (int and int) to binary operator &&

-AttributeTyping.bpl(11,22): Error: invalid argument type (int) to unary operator !

-AttributeTyping.bpl(13,32): Error: invalid argument types (int and int) to binary operator ==>

-6 type checking errors detected in AttributeTyping.bpl

-UpdateExprTyping.bpl(3,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

-UpdateExprTyping.bpl(4,11): Error: invalid argument types ([int]bool and [bool]bool) to binary operator ==

-UpdateExprTyping.bpl(7,16): Error: invalid type for argument 0 in map store: bool (expected: int)

-UpdateExprTyping.bpl(8,21): Error: right-hand side in map store with wrong type: int (expected: bool)

-UpdateExprTyping.bpl(9,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

-UpdateExprTyping.bpl(15,18): Error: invalid type for argument 0 in map store: ref (expected: int)

-UpdateExprTyping.bpl(16,20): Error: invalid type for argument 1 in map store: bool (expected: ref)

-UpdateExprTyping.bpl(17,28): Error: right-hand side in map store with wrong type: ref (expected: bool)

-UpdateExprTyping.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to any)

-UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type: ref (expected: any)

-UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)

-UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)

-12 type checking errors detected in UpdateExprTyping.bpl

-CallForallResolve.bpl(15,2): Error: call forall is allowed only on procedures with no modifies clause: Q

-1 type checking errors detected in CallForallResolve.bpl

-MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m

-MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)

-MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)

-MapsTypeErrors.bpl(39,3): Error: mismatched types in assignment command (cannot assign bool to int)

-MapsTypeErrors.bpl(67,14): Error: invalid argument types (Field int and Field bool) to binary operator ==

-MapsTypeErrors.bpl(70,27): Error: invalid type for argument 1 in application of StrictEqual: Field bool (expected: a)

-MapsTypeErrors.bpl(75,33): Error: invalid type for argument 1 in application of StrictEqual: Field int (expected: a)

-MapsTypeErrors.bpl(77,31): Error: invalid type for argument 1 in application of IntEqual: Field alpha (expected: Field int)

-MapsTypeErrors.bpl(90,8): Error: extract operand must be a bitvector of at least 32 bits (got bv31)

-MapsTypeErrors.bpl(91,8): Error: extract operand must be a bitvector of at least 32 bits (got int)

-MapsTypeErrors.bpl(95,2): Error: mismatched types in assignment command (cannot assign bv33 to bv32)

-MapsTypeErrors.bpl(104,2): Error: mismatched types in assignment command (cannot assign bv20 to bv32)

-MapsTypeErrors.bpl(110,56): Error: invalid type for argument 1 in application of Same: bv18 (expected: T)

-MapsTypeErrors.bpl(120,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to [int,int]bool)

-MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to HeapType)

-15 type checking errors detected in MapsTypeErrors.bpl

-Orderings.bpl(6,19): Error: parent of constant has incompatible type (int instead of C)

-1 type checking errors detected in Orderings.bpl

-EmptyCallArgs.bpl(15,17): Error: invalid type for argument 0 in call to P: int (expected: bool)

-EmptyCallArgs.bpl(26,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

-EmptyCallArgs.bpl(28,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

-3 type checking errors detected in EmptyCallArgs.bpl

-FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)

-FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)

-FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)

-3 type checking errors detected in FunBody.bpl

diff --git a/Test/test13/Output b/Test/test13/Output
deleted file mode 100644
index c8263ac1..00000000
--- a/Test/test13/Output
+++ /dev/null
@@ -1,15 +0,0 @@
-

--------------------- ErrorTraceTestLoopInvViolationBPL --------------------

-ErrorTraceTestLoopInvViolationBPL.bpl(7,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ErrorTraceTestLoopInvViolationBPL.bpl(5,5): anon0

-ErrorTraceTestLoopInvViolationBPL.bpl(16,16): Error BP5004: This loop invariant might not hold on entry.

-Execution trace:

-    ErrorTraceTestLoopInvViolationBPL.bpl(14,5): anon0

-ErrorTraceTestLoopInvViolationBPL.bpl(27,17): Error BP5005: This loop invariant might not be maintained by the loop.

-Execution trace:

-    ErrorTraceTestLoopInvViolationBPL.bpl(25,5): anon0

-    ErrorTraceTestLoopInvViolationBPL.bpl(27,3): anon2_LoopHead

-    ErrorTraceTestLoopInvViolationBPL.bpl(28,7): anon2_LoopBody

-

-Boogie program verifier finished with 0 verified, 3 errors

diff --git a/Test/test15/Output b/Test/test15/Output
deleted file mode 100644
index 2054998f..00000000
--- a/Test/test15/Output
+++ /dev/null
@@ -1,177 +0,0 @@
-

--------------------- NullInModel --------------------

-Z3 error model: 

-partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 3:int

-*3 {@false} -> 4:int

-*4 {intType} 

-*5 {boolType} 

-*6 {refType} 

-*7 {s null} 

-*8 -> 0:int

-*9 -> 1:int

-*10 -> 2:int

-*11 

-function interpretations:

-$pow2 -> {

-  *8 -> *9

-  else -> #unspecified

-}

-Ctor -> {

-  *4 -> *8

-  *5 -> *9

-  *6 -> *10

-  else -> #unspecified

-}

-type -> {

-  *7 -> *6

-  else -> #unspecified

-}

-END_OF_MODEL

-.

-identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

-refType : *6

-s : *7

-null : *7

-valueToPartition:

-True : *0

-False : *1

-3 : *2

-4 : *3

-0 : *8

-1 : *9

-2 : *10

-End of model.

-NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NullInModel.bpl(2,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- IntInModel --------------------

-Z3 error model: 

-partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 2:int

-*3 {@false} -> 3:int

-*4 {intType} 

-*5 {boolType} 

-*6 {i} -> 0:int

-*7 -> 1:int

-*8 

-function interpretations:

-$pow2 -> {

-  *6 -> *7

-  else -> #unspecified

-}

-Ctor -> {

-  *4 -> *6

-  *5 -> *7

-  else -> #unspecified

-}

-END_OF_MODEL

-.

-identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

-i : *6

-valueToPartition:

-True : *0

-False : *1

-2 : *2

-3 : *3

-0 : *6

-1 : *7

-End of model.

-IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    IntInModel.bpl(2,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- ModelTest --------------------

-Z3 error model: 

-partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 5:int

-*3 {@false} -> 6:int

-*4 {intType} 

-*5 {boolType} 

-*6 {refType} 

-*7 {s} 

-*8 {r} 

-*9 {i@0} -> 1:int

-*10 {j@0} -> 2:int

-*11 {j@1} -> 3:int

-*12 {j@2} -> 4:int

-*13 -> 0:int

-*14 

-function interpretations:

-$pow2 -> {

-  *13 -> *9

-  else -> #unspecified

-}

-Ctor -> {

-  *4 -> *13

-  *5 -> *9

-  *6 -> *10

-  else -> #unspecified

-}

-type -> {

-  *7 -> *6

-  *8 -> *6

-  else -> #unspecified

-}

-END_OF_MODEL

-.

-identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

-refType : *6

-s : *7

-r : *8

-i@0 : *9

-j@0 : *10

-j@1 : *11

-j@2 : *12

-valueToPartition:

-True : *0

-False : *1

-5 : *2

-6 : *3

-1 : *9

-2 : *10

-3 : *11

-4 : *12

-0 : *13

-End of model.

-ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ModelTest.bpl(3,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- InterpretedFunctionTests --------------------

-InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterpretedFunctionTests.bpl(2,3): anon0

-InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterpretedFunctionTests.bpl(8,3): anon0

-InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterpretedFunctionTests.bpl(14,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

diff --git a/Test/test16/Output b/Test/test16/Output
deleted file mode 100644
index 5fac425b..00000000
--- a/Test/test16/Output
+++ /dev/null
@@ -1,23 +0,0 @@
--------------------- LoopUnroll.bpl /loopUnroll:1 --------------------

-LoopUnroll.bpl(56,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    LoopUnroll.bpl(52,5): anon0#1

-    LoopUnroll.bpl(53,3): anon2_LoopHead#1

-    LoopUnroll.bpl(55,5): anon2_LoopBody#1

-

-Boogie program verifier finished with 2 verified, 1 error

--------------------- LoopUnroll.bpl /loopUnroll:2 --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- LoopUnroll.bpl /loopUnroll:3 --------------------

-LoopUnroll.bpl(74,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    LoopUnroll.bpl(68,5): anon0#3

-    LoopUnroll.bpl(69,3): anon2_LoopHead#3

-    LoopUnroll.bpl(71,5): anon2_LoopBody#3

-    LoopUnroll.bpl(69,3): anon2_LoopHead#2

-    LoopUnroll.bpl(71,5): anon2_LoopBody#2

-    LoopUnroll.bpl(69,3): anon2_LoopHead#1

-    LoopUnroll.bpl(71,5): anon2_LoopBody#1

-

-Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/test2/Output b/Test/test2/Output
deleted file mode 100644
index 7876d732..00000000
--- a/Test/test2/Output
+++ /dev/null
@@ -1,359 +0,0 @@
-

--------------------- FormulaTerm.bpl --------------------

-FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement.

-FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    FormulaTerm.bpl(8,1): start

-

-Boogie program verifier finished with 11 verified, 1 error

-

--------------------- FormulaTerm2.bpl --------------------

-FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    FormulaTerm2.bpl(36,3): start

-FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    FormulaTerm2.bpl(45,3): start

-

-Boogie program verifier finished with 2 verified, 2 errors

-

--------------------- Passification.bpl --------------------

-Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement.

-Passification.bpl(36,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Passification.bpl(39,1): A

-Passification.bpl(116,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Passification.bpl(106,1): L0

-    Passification.bpl(111,1): L1

-    Passification.bpl(115,1): L2

-Passification.bpl(151,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Passification.bpl(144,1): L0

-    Passification.bpl(150,1): L2

-Passification.bpl(165,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Passification.bpl(158,1): L0

-    Passification.bpl(161,1): L1

-    Passification.bpl(164,1): L2

-

-Boogie program verifier finished with 7 verified, 4 errors

-

--------------------- B.bpl --------------------

-

-Boogie program verifier finished with 4 verified, 0 errors

-

--------------------- Ensures.bpl --------------------

-Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement.

-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Ensures.bpl(28,3): start

-Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement.

-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Ensures.bpl(34,3): start

-Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement.

-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Ensures.bpl(39,3): start

-Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement.

-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Ensures.bpl(45,3): start

-Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement.

-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Ensures.bpl(70,3): start

-

-Boogie program verifier finished with 5 verified, 5 errors

-

--------------------- Old.bpl --------------------

-Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement.

-Old.bpl(26,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Old.bpl(28,3): start

-

-Boogie program verifier finished with 7 verified, 1 error

-

--------------------- OldIllegal.bpl --------------------

-OldIllegal.bpl(7,11): Error: old expressions allowed only in two-state contexts

-OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts

-2 name resolution errors detected in OldIllegal.bpl

-

--------------------- Arrays.bpl --------------------

-Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement.

-Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Arrays.bpl(42,3): start

-Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement.

-Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Arrays.bpl(123,3): start

-

-Boogie program verifier finished with 8 verified, 2 errors

-

--------------------- Axioms.bpl --------------------

-Axioms.bpl(19,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Axioms.bpl(18,3): start

-

-Boogie program verifier finished with 2 verified, 1 error

-

--------------------- Quantifiers.bpl --------------------

-Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Quantifiers.bpl(19,3): start

-Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Quantifiers.bpl(42,3): start

-Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Quantifiers.bpl(64,3): start

-Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Quantifiers.bpl(71,3): start

-Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Quantifiers.bpl(124,3): start

-Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Quantifiers.bpl(149,3): start

-

-Boogie program verifier finished with 8 verified, 6 errors

-

--------------------- Call.bpl --------------------

-Call.bpl(13,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Call.bpl(9,3): entry

-Call.bpl(46,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    Call.bpl(45,3): start

-Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement.

-Call.bpl(20,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Call.bpl(53,3): start

-

-Boogie program verifier finished with 2 verified, 3 errors

-

--------------------- AssumeEnsures.bpl --------------------

-AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold.

-Execution trace:

-    AssumeEnsures.bpl(26,5): entry

-AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold.

-Execution trace:

-    AssumeEnsures.bpl(46,5): entry

-AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold.

-Execution trace:

-    AssumeEnsures.bpl(60,5): entry

-

-Boogie program verifier finished with 4 verified, 3 errors

-

--------------------- CutBackEdge.bpl --------------------

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

-Execution trace:

-    CutBackEdge.bpl(5,3): entry

-    CutBackEdge.bpl(9,3): block850

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- False.bpl --------------------

-

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- LoopInvAssume.bpl --------------------

-LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold.

-Execution trace:

-    LoopInvAssume.bpl(8,4): entry

-    LoopInvAssume.bpl(16,4): exit

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- strings-no-where.bpl --------------------

-strings-no-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator ==

-strings-no-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator ==

-strings-no-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)

-strings-no-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)

-strings-no-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)

-strings-no-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)

-strings-no-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)

-strings-no-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator ==

-strings-no-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator ==

-strings-no-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)

-strings-no-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-no-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-no-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-no-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-no-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator ==

-strings-no-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator ==

-strings-no-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any)

-strings-no-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator ==

-18 type checking errors detected in strings-no-where.bpl

-

--------------------- strings-where.bpl --------------------

-strings-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator ==

-strings-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator ==

-strings-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)

-strings-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)

-strings-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)

-strings-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)

-strings-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)

-strings-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator ==

-strings-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator ==

-strings-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)

-strings-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any)

-strings-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator ==

-strings-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator ==

-strings-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any)

-strings-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator ==

-18 type checking errors detected in strings-where.bpl

-

--------------------- Structured.bpl --------------------

-Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement.

-Structured.bpl(243,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    Structured.bpl(245,3): anon0

-    Structured.bpl(245,3): anon6_LoopHead

-    Structured.bpl(246,5): anon6_LoopBody

-    Structured.bpl(247,7): anon7_LoopBody

-    Structured.bpl(252,5): anon4

-    Structured.bpl(252,14): anon9_Then

-Structured.bpl(303,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Structured.bpl(299,5): anon0

-    Structured.bpl(300,3): anon3_Else

-    Structured.bpl(303,3): anon2

-Structured.bpl(311,7): Error BP5001: This assertion might not hold.

-Execution trace:

-    Structured.bpl(308,3): anon0

-    Structured.bpl(308,3): anon1_Then

-    Structured.bpl(309,5): A

-

-Boogie program verifier finished with 15 verified, 3 errors

-

--------------------- Where.bpl --------------------

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

-Execution trace:

-    Where.bpl(6,3): anon0

-Where.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(16,5): anon0

-Where.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(30,3): anon0

-Where.bpl(44,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(40,5): anon0

-Where.bpl(57,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(52,3): anon0

-Where.bpl(111,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(102,5): anon0

-    Where.bpl(104,3): anon3_LoopHead

-    Where.bpl(110,3): anon2

-Where.bpl(128,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(121,5): anon0

-    Where.bpl(122,3): anon3_LoopHead

-    Where.bpl(125,3): anon2

-Where.bpl(145,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(138,5): anon0

-    Where.bpl(139,3): anon3_LoopHead

-    Where.bpl(142,3): anon2

-Where.bpl(162,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Where.bpl(155,5): anon0

-    Where.bpl(156,3): anon3_LoopHead

-    Where.bpl(159,3): anon2

-

-Boogie program verifier finished with 2 verified, 9 errors

-

--------------------- UpdateExpr.bpl --------------------

-UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    UpdateExpr.bpl(14,3): anon0

-UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    UpdateExpr.bpl(19,3): anon0

-UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    UpdateExpr.bpl(32,3): anon0

-UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    UpdateExpr.bpl(38,3): anon0

-UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    UpdateExpr.bpl(51,5): anon0

-

-Boogie program verifier finished with 5 verified, 5 errors

-

--------------------- NeverPattern.bpl --------------------

-NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NeverPattern.bpl(15,3): anon0

-NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NeverPattern.bpl(21,3): anon0

-NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NeverPattern.bpl(27,3): anon0

-

-Boogie program verifier finished with 1 verified, 3 errors

-

--------------------- NullaryMaps.bpl --------------------

-NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NullaryMaps.bpl(28,3): anon0

-NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NullaryMaps.bpl(28,3): anon0

-NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NullaryMaps.bpl(36,3): anon0

-

-Boogie program verifier finished with 2 verified, 3 errors

-

--------------------- Implies.bpl --------------------

-Implies.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Implies.bpl(11,3): anon0

-Implies.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Implies.bpl(11,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

--------------------- sk_hack.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

-

--------------------- CallForall.bpl --------------------

-CallForall.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(17,3): anon0

-CallForall.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(28,3): anon0

-CallForall.bpl(41,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(40,3): anon0

-CallForall.bpl(47,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(46,3): anon0

-CallForall.bpl(75,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(75,3): anon0

-CallForall.bpl(111,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(109,3): anon0

-CallForall.bpl(118,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(117,3): anon0

-CallForall.bpl(125,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    CallForall.bpl(124,3): anon0

-

-Boogie program verifier finished with 10 verified, 8 errors

diff --git a/Test/test20/Output b/Test/test20/Output
deleted file mode 100644
index a4b991f7..00000000
--- a/Test/test20/Output
+++ /dev/null
@@ -1,192 +0,0 @@
-TypeDecls0.bpl(20,5): Error: more than one declaration of type name: C

-TypeDecls0.bpl(13,12): Error: more than one declaration of type variable: a

-TypeDecls0.bpl(14,18): Error: more than one declaration of type variable: a

-TypeDecls0.bpl(18,17): Error: type variable must occur in map arguments: b

-TypeDecls0.bpl(22,9): Error: type constructor received wrong number of arguments: C

-TypeDecls0.bpl(24,9): Error: undeclared type: A0

-TypeDecls0.bpl(25,9): Error: undeclared type: F

-TypeDecls0.bpl(28,9): Error: type constructor received wrong number of arguments: E

-TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E

-TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E

-TypeDecls0.bpl(38,11): Error: type constructor received wrong number of arguments: E

-TypeDecls0.bpl(38,13): Error: type constructor received wrong number of arguments: E

-12 name resolution errors detected in TypeDecls0.bpl

-TypeDecls1.bpl(7,13): Error: invalid type for argument 0 in map select: int (expected: <b>[b]a)

-TypeDecls1.bpl(13,25): Error: right-hand side in map store with wrong type: int (expected: bool)

-TypeDecls1.bpl(19,36): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

-TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)

-4 type checking errors detected in TypeDecls1.bpl

-Prog0.bpl(17,10): Error: type variable must occur in map arguments: a

-Prog0.bpl(29,27): Error: more than one declaration of type variable: beta

-Prog0.bpl(32,22): Error: undeclared type: alpha

-Prog0.bpl(33,35): Error: undeclared type: alpha

-4 name resolution errors detected in Prog0.bpl

-Prog1.bpl(18,11): Error: invalid type for argument 0 in map select: int (expected: ref)

-Prog1.bpl(19,14): Error: invalid type for argument 1 in map select: int (expected: Field a)

-Prog1.bpl(20,17): Error: invalid argument types (bool and int) to binary operator >=

-3 type checking errors detected in Prog1.bpl

-Prog2.bpl(6,14): Error: trigger does not mention alpha, which does not occur in variables types either

-1 type checking errors detected in Prog2.bpl

-PolyFuns0.bpl(23,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a)

-PolyFuns0.bpl(40,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a)

-PolyFuns0.bpl(41,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a)

-PolyFuns0.bpl(53,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

-4 type checking errors detected in PolyFuns0.bpl

-PolyFuns1.bpl(10,9): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(17,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

-PolyFuns1.bpl(18,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

-PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)

-PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)

-PolyFuns1.bpl(30,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==

-PolyFuns1.bpl(31,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==

-PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)

-PolyFuns1.bpl(41,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==

-PolyFuns1.bpl(42,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==

-PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==

-PolyFuns1.bpl(50,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[a,b,b]int) to binary operator ==

-PolyFuns1.bpl(57,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator ==

-16 type checking errors detected in PolyFuns1.bpl

-PolyProcs0.bpl(11,16): Error: invalid type for argument 0 in map select: Field b (expected: ref)

-PolyProcs0.bpl(11,19): Error: invalid type for argument 1 in map select: ref (expected: Field a)

-PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref)

-PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)

-PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)

-PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)

-PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)

-7 type checking errors detected in PolyProcs0.bpl

-TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)

-TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)

-TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)

-TypeSynonyms0.bpl(22,10): Error: type constructor received wrong number of arguments: Field

-TypeSynonyms0.bpl(23,10): Error: type synonym received wrong number of arguments: Set

-TypeSynonyms0.bpl(26,10): Error: type variable must occur in map arguments: a

-6 name resolution errors detected in TypeSynonyms0.bpl

-TypeSynonyms1.bpl(46,8): Error: invalid type for argument 0 in application of h: <b>[b,b,<b2>[b2,b,int]int]int (expected: nested2)

-1 type checking errors detected in TypeSynonyms1.bpl

-

-Boogie program verifier finished with 1 verified, 0 errors

-

-type Set a = [a]bool;

-

-type Field _;

-

-type Heap = <a>[ref,Field a]a;

-

-type notAllParams a b = Field b;

-

-type Cyclic0 = Cyclic1;

-

-type Cyclic1 = Cyclic0;

-

-type AlsoCyclic a = <b>[AlsoCyclic b]int;

-

-type C _ _;

-

-type C2 b a = C a b;

-

-function f(C int bool) returns (int);

-

-const x: C2 bool int;

-

-const y: Field int bool;

-

-const z: Set int bool;

-

-const d: <a,b>[notAllParams a b]int;

-

-type ref;

-<console>(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)

-<console>(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)

-<console>(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)

-<console>(24,8): Error: type constructor received wrong number of arguments: Field

-<console>(26,8): Error: type synonym received wrong number of arguments: Set

-<console>(28,8): Error: type variable must occur in map arguments: a

-6 name resolution errors detected in TypeSynonyms0.bpl

-

-type Set a = [a]bool;

-

-function union<a>(x: Set a, y: Set a) returns (Set a);

-

-axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);

-

-const intSet0: Set int;

-

-axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));

-

-const intSet1: Set int;

-

-axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));

-

-procedure P();

-

-

-

-implementation P()

-{

-    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));

-}

-

-

-

-type Set a = [a]bool;

-

-function union<a>(x: Set a, y: Set a) returns (Set a);

-

-axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);

-

-const intSet0: Set int;

-

-axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);

-

-const intSet1: Set int;

-

-axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);

-

-procedure P();

-

-

-

-implementation P()

-{

-    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

-PolyPolyPoly.bpl(12,26): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==

-PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==

-PolyPolyPoly.bpl(21,57): Error: invalid type for argument 1 in map select: b (expected: a)

-3 type checking errors detected in PolyPolyPoly.bpl

-PolyPolyPoly2.bpl(5,8): Warning: type parameter a is ambiguous, instantiating to int

-PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to <arg0,res>[arg0]res

-PolyPolyPoly2.bpl(11,8): Warning: type parameter a is ambiguous, instantiating to bv0

-PolyPolyPoly2.bpl(11,15): Warning: type parameter a is ambiguous, instantiating to bv0

-PolyPolyPoly2.bpl(11,27): Warning: type parameter a is ambiguous, instantiating to bv17

-PolyPolyPoly2.bpl(12,8): Warning: type parameter a is ambiguous, instantiating to bv17

-PolyPolyPoly2.bpl(12,15): Warning: type parameter a is ambiguous, instantiating to bv0

-PolyPolyPoly2.bpl(22,7): Warning: type parameter a is ambiguous, instantiating to int

-PolyPolyPoly2.bpl(31,3): Warning: type parameter a is ambiguous, instantiating to int

-PolyPolyPoly2.bpl(32,3): Warning: type parameter a is ambiguous, instantiating to int

-

-Boogie program verifier finished with 0 verified, 0 errors

-ProcParamReordering.bpl(13,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation)

-ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in procedure implementation: P

-2 type checking errors detected in ProcParamReordering.bpl

-ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int)

-ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z

-3 type checking errors detected in ParallelAssignment.bpl

-ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides

-ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment

-2 name resolution errors detected in ParallelAssignment2.bpl

-Coercions.bpl(11,8): Error: int cannot be coerced to E <a>[a]int

-Coercions.bpl(13,8): Error: C cannot be coerced to D

-Coercions.bpl(15,9): Error: int cannot be coerced to D

-Coercions.bpl(16,9): Error: int cannot be coerced to E int

-4 type checking errors detected in Coercions.bpl

-

-Boogie program verifier finished with 0 verified, 0 errors

diff --git a/Test/test21/Output b/Test/test21/Output
deleted file mode 100644
index bda444d2..00000000
--- a/Test/test21/Output
+++ /dev/null
@@ -1,1677 +0,0 @@
---------------------- TypeEncoding n ----------------------------

---------------------- File DisjointDomains.bpl ----------------------------

-

-Boogie program verifier finished with 3 verified, 0 errors

---------------------- File DisjointDomains2.bpl ----------------------------

-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(9,3): start

-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(16,3): start

-

-Boogie program verifier finished with 4 verified, 2 errors

---------------------- File FunAxioms.bpl ----------------------------

-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File FunAxioms2.bpl ----------------------------

-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms2.bpl(16,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File PolyList.bpl ----------------------------

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

-Execution trace:

-    PolyList.bpl(27,7): anon0

-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    PolyList.bpl(49,7): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Maps0.bpl ----------------------------

-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(14,3): anon0

-Maps0.bpl(46,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-Maps0.bpl(49,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-Maps0.bpl(52,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-

-Boogie program verifier finished with 1 verified, 5 errors

---------------------- File Maps1.bpl ----------------------------

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

-Execution trace:

-    Maps1.bpl(19,3): anon0

-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps1.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples0.bpl ----------------------------

-InterestingExamples0.bpl(7,1): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples0.bpl(5,6): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples1.bpl ----------------------------

-InterestingExamples1.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples2.bpl ----------------------------

-InterestingExamples2.bpl(9,1): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples2.bpl(8,6): anon0

-InterestingExamples2.bpl(10,1): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples2.bpl(8,6): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples3.bpl ----------------------------

-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples3.bpl(13,2): anon0

-

-Boogie program verifier finished with 2 verified, 1 error

---------------------- File InterestingExamples4.bpl ----------------------------

-InterestingExamples4.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples5.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Colors.bpl ----------------------------

-Colors.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(12,3): anon0

-Colors.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File HeapAbstraction.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File HeapAxiom.bpl ----------------------------

-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAxiom.bpl(13,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Triggers0.bpl ----------------------------

-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-

-Boogie program verifier finished with 1 verified, 2 errors

---------------------- File Triggers1.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Casts.bpl ----------------------------

-Casts.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Casts.bpl(6,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptyList.bpl ----------------------------

-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int

-EmptyList.bpl(28,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptyList.bpl(26,5): anon0

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

-Execution trace:

-    EmptyList.bpl(26,5): anon0

-EmptyList.bpl(46,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptyList.bpl(46,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Boxing.bpl ----------------------------

-Boxing.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File MapOutputTypeParams.bpl ----------------------------

-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int

-MapOutputTypeParams.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-

-Boogie program verifier finished with 0 verified, 6 errors

---------------------- File ParallelAssignment.bpl ----------------------------

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

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(40,11): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File BooleanQuantification.bpl ----------------------------

-BooleanQuantification.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(10,3): anon0

-BooleanQuantification.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-

-Boogie program verifier finished with 1 verified, 5 errors

---------------------- File BooleanQuantification2.bpl ----------------------------

-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification2.bpl(10,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Flattening.bpl ----------------------------

-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Flattening.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings.bpl ----------------------------

-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings.bpl(9,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Orderings2.bpl ----------------------------

-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings2.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings3.bpl ----------------------------

-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(15,3): anon0

-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Orderings4.bpl ----------------------------

-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings4.bpl(9,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptySetBug.bpl ----------------------------

-EmptySetBug.bpl(27,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Coercions2.bpl ----------------------------

-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int

-Coercions2.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File MapAxiomsConsistency.bpl ----------------------------

-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapAxiomsConsistency.bpl(79,13): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File NameClash.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File LetSorting.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- TypeEncoding p ----------------------------

---------------------- File DisjointDomains.bpl ----------------------------

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

-Execution trace:

-    DisjointDomains.bpl(11,3): start

-DisjointDomains.bpl(21,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(20,3): start

-DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(26,3): start

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File DisjointDomains2.bpl ----------------------------

-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(9,3): start

-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(16,3): start

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

-Execution trace:

-    DisjointDomains2.bpl(30,3): start

-DisjointDomains2.bpl(39,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(37,3): start

-DisjointDomains2.bpl(49,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(45,3): start

-DisjointDomains2.bpl(63,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(58,3): start

-

-Boogie program verifier finished with 0 verified, 6 errors

---------------------- File FunAxioms.bpl ----------------------------

-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File FunAxioms2.bpl ----------------------------

-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms2.bpl(16,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File PolyList.bpl ----------------------------

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

-Execution trace:

-    PolyList.bpl(27,7): anon0

-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    PolyList.bpl(49,7): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Maps0.bpl ----------------------------

-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(14,3): anon0

-Maps0.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(32,3): anon0

-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Maps1.bpl ----------------------------

-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps1.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples0.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples1.bpl ----------------------------

-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples2.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples3.bpl ----------------------------

-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples3.bpl(13,2): anon0

-

-Boogie program verifier finished with 2 verified, 1 error

---------------------- File InterestingExamples4.bpl ----------------------------

-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples5.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Colors.bpl ----------------------------

-Colors.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(12,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File HeapAbstraction.bpl ----------------------------

-HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAbstraction.bpl(14,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File HeapAxiom.bpl ----------------------------

-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAxiom.bpl(13,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Triggers0.bpl ----------------------------

-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-

-Boogie program verifier finished with 1 verified, 2 errors

---------------------- File Triggers1.bpl ----------------------------

-Triggers1.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers1.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Casts.bpl ----------------------------

-Casts.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Casts.bpl(6,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptyList.bpl ----------------------------

-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int

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

-Execution trace:

-    EmptyList.bpl(26,5): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Boxing.bpl ----------------------------

-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapOutputTypeParams.bpl ----------------------------

-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int

-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File ParallelAssignment.bpl ----------------------------

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

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(40,11): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File BooleanQuantification.bpl ----------------------------

-BooleanQuantification.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(10,3): anon0

-BooleanQuantification.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-

-Boogie program verifier finished with 1 verified, 5 errors

---------------------- File BooleanQuantification2.bpl ----------------------------

-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification2.bpl(10,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Flattening.bpl ----------------------------

-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Flattening.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings.bpl ----------------------------

-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings.bpl(9,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Orderings2.bpl ----------------------------

-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings2.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings3.bpl ----------------------------

-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(15,3): anon0

-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Orderings4.bpl ----------------------------

-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings4.bpl(9,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptySetBug.bpl ----------------------------

-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Coercions2.bpl ----------------------------

-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int

-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapAxiomsConsistency.bpl ----------------------------

-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapAxiomsConsistency.bpl(79,13): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File NameClash.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File LetSorting.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- TypeEncoding a ----------------------------

---------------------- File DisjointDomains.bpl ----------------------------

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

-Execution trace:

-    DisjointDomains.bpl(11,3): start

-DisjointDomains.bpl(21,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(20,3): start

-DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(26,3): start

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File DisjointDomains2.bpl ----------------------------

-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(9,3): start

-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(16,3): start

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

-Execution trace:

-    DisjointDomains2.bpl(30,3): start

-DisjointDomains2.bpl(39,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(37,3): start

-DisjointDomains2.bpl(49,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(45,3): start

-DisjointDomains2.bpl(63,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(58,3): start

-

-Boogie program verifier finished with 0 verified, 6 errors

---------------------- File FunAxioms.bpl ----------------------------

-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File FunAxioms2.bpl ----------------------------

-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms2.bpl(16,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File PolyList.bpl ----------------------------

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

-Execution trace:

-    PolyList.bpl(27,7): anon0

-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    PolyList.bpl(49,7): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Maps0.bpl ----------------------------

-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(14,3): anon0

-Maps0.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(32,3): anon0

-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Maps1.bpl ----------------------------

-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps1.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples0.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples1.bpl ----------------------------

-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples2.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples3.bpl ----------------------------

-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples3.bpl(13,2): anon0

-

-Boogie program verifier finished with 2 verified, 1 error

---------------------- File InterestingExamples4.bpl ----------------------------

-InterestingExamples4.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples5.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Colors.bpl ----------------------------

-Colors.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(12,3): anon0

-Colors.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File HeapAbstraction.bpl ----------------------------

-HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAbstraction.bpl(14,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File HeapAxiom.bpl ----------------------------

-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAxiom.bpl(13,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Triggers0.bpl ----------------------------

-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-

-Boogie program verifier finished with 1 verified, 2 errors

---------------------- File Triggers1.bpl ----------------------------

-Triggers1.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers1.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Casts.bpl ----------------------------

-Casts.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Casts.bpl(6,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptyList.bpl ----------------------------

-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int

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

-Execution trace:

-    EmptyList.bpl(26,5): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Boxing.bpl ----------------------------

-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapOutputTypeParams.bpl ----------------------------

-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int

-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File ParallelAssignment.bpl ----------------------------

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

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(40,11): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File BooleanQuantification.bpl ----------------------------

-BooleanQuantification.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(10,3): anon0

-BooleanQuantification.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-

-Boogie program verifier finished with 1 verified, 5 errors

---------------------- File BooleanQuantification2.bpl ----------------------------

-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification2.bpl(10,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Flattening.bpl ----------------------------

-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Flattening.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings.bpl ----------------------------

-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings.bpl(9,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Orderings2.bpl ----------------------------

-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings2.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings3.bpl ----------------------------

-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(15,3): anon0

-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Orderings4.bpl ----------------------------

-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings4.bpl(9,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptySetBug.bpl ----------------------------

-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Coercions2.bpl ----------------------------

-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int

-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapAxiomsConsistency.bpl ----------------------------

-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapAxiomsConsistency.bpl(79,13): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File NameClash.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File LetSorting.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- TypeEncoding n z3types ----------------------------

---------------------- File DisjointDomains.bpl ----------------------------

-

-Boogie program verifier finished with 3 verified, 0 errors

---------------------- File DisjointDomains2.bpl ----------------------------

-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(9,3): start

-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(16,3): start

-

-Boogie program verifier finished with 4 verified, 2 errors

---------------------- File FunAxioms.bpl ----------------------------

-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File FunAxioms2.bpl ----------------------------

-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms2.bpl(16,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File PolyList.bpl ----------------------------

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

-Execution trace:

-    PolyList.bpl(27,7): anon0

-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    PolyList.bpl(49,7): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Maps0.bpl ----------------------------

-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(14,3): anon0

-Maps0.bpl(46,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-Maps0.bpl(49,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-Maps0.bpl(52,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-

-Boogie program verifier finished with 1 verified, 5 errors

---------------------- File Maps1.bpl ----------------------------

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

-Execution trace:

-    Maps1.bpl(19,3): anon0

-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps1.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples0.bpl ----------------------------

-InterestingExamples0.bpl(7,1): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples0.bpl(5,6): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples1.bpl ----------------------------

-InterestingExamples1.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples2.bpl ----------------------------

-InterestingExamples2.bpl(9,1): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples2.bpl(8,6): anon0

-InterestingExamples2.bpl(10,1): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples2.bpl(8,6): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples3.bpl ----------------------------

-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples3.bpl(13,2): anon0

-

-Boogie program verifier finished with 2 verified, 1 error

---------------------- File InterestingExamples4.bpl ----------------------------

-InterestingExamples4.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples5.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Colors.bpl ----------------------------

-Colors.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(12,3): anon0

-Colors.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File HeapAbstraction.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File HeapAxiom.bpl ----------------------------

-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAxiom.bpl(13,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Triggers0.bpl ----------------------------

-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-

-Boogie program verifier finished with 1 verified, 2 errors

---------------------- File Triggers1.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Casts.bpl ----------------------------

-Casts.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Casts.bpl(6,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File BooleanQuantification.bpl ----------------------------

-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-

-Boogie program verifier finished with 2 verified, 2 errors

---------------------- File EmptyList.bpl ----------------------------

-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int

-EmptyList.bpl(28,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptyList.bpl(26,5): anon0

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

-Execution trace:

-    EmptyList.bpl(26,5): anon0

-EmptyList.bpl(46,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptyList.bpl(46,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Boxing.bpl ----------------------------

-Boxing.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File MapOutputTypeParams.bpl ----------------------------

-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int

-MapOutputTypeParams.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-

-Boogie program verifier finished with 0 verified, 6 errors

---------------------- File ParallelAssignment.bpl ----------------------------

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

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(40,11): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File BooleanQuantification2.bpl ----------------------------

-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification2.bpl(10,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Flattening.bpl ----------------------------

-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Flattening.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings.bpl ----------------------------

-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings.bpl(9,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Orderings2.bpl ----------------------------

-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings2.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings3.bpl ----------------------------

-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(15,3): anon0

-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Orderings4.bpl ----------------------------

-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings4.bpl(9,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptySetBug.bpl ----------------------------

-EmptySetBug.bpl(27,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Coercions2.bpl ----------------------------

-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int

-Coercions2.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File MapAxiomsConsistency.bpl ----------------------------

-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapAxiomsConsistency.bpl(79,13): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LetSorting.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- TypeEncoding p z3types ----------------------------

---------------------- File DisjointDomains.bpl ----------------------------

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

-Execution trace:

-    DisjointDomains.bpl(11,3): start

-DisjointDomains.bpl(21,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(20,3): start

-DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(26,3): start

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File DisjointDomains2.bpl ----------------------------

-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(9,3): start

-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(16,3): start

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

-Execution trace:

-    DisjointDomains2.bpl(30,3): start

-DisjointDomains2.bpl(39,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(37,3): start

-DisjointDomains2.bpl(49,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(45,3): start

-DisjointDomains2.bpl(63,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(58,3): start

-

-Boogie program verifier finished with 0 verified, 6 errors

---------------------- File FunAxioms.bpl ----------------------------

-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File FunAxioms2.bpl ----------------------------

-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms2.bpl(16,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File PolyList.bpl ----------------------------

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

-Execution trace:

-    PolyList.bpl(27,7): anon0

-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    PolyList.bpl(49,7): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Maps0.bpl ----------------------------

-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(14,3): anon0

-Maps0.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(32,3): anon0

-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Maps1.bpl ----------------------------

-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps1.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples0.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples1.bpl ----------------------------

-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples2.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples3.bpl ----------------------------

-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples3.bpl(13,2): anon0

-

-Boogie program verifier finished with 2 verified, 1 error

---------------------- File InterestingExamples4.bpl ----------------------------

-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples5.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Colors.bpl ----------------------------

-Colors.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(12,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File HeapAbstraction.bpl ----------------------------

-HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAbstraction.bpl(14,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File HeapAxiom.bpl ----------------------------

-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAxiom.bpl(13,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Triggers0.bpl ----------------------------

-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-

-Boogie program verifier finished with 1 verified, 2 errors

---------------------- File Triggers1.bpl ----------------------------

-Triggers1.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers1.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Casts.bpl ----------------------------

-Casts.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Casts.bpl(6,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File BooleanQuantification.bpl ----------------------------

-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-

-Boogie program verifier finished with 2 verified, 2 errors

---------------------- File EmptyList.bpl ----------------------------

-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int

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

-Execution trace:

-    EmptyList.bpl(26,5): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Boxing.bpl ----------------------------

-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapOutputTypeParams.bpl ----------------------------

-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int

-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File ParallelAssignment.bpl ----------------------------

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

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(40,11): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File BooleanQuantification2.bpl ----------------------------

-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification2.bpl(10,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Flattening.bpl ----------------------------

-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Flattening.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings.bpl ----------------------------

-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings.bpl(9,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Orderings2.bpl ----------------------------

-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings2.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings3.bpl ----------------------------

-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(15,3): anon0

-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Orderings4.bpl ----------------------------

-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings4.bpl(9,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptySetBug.bpl ----------------------------

-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Coercions2.bpl ----------------------------

-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int

-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapAxiomsConsistency.bpl ----------------------------

-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapAxiomsConsistency.bpl(79,13): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LetSorting.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- TypeEncoding a z3types ----------------------------

---------------------- File DisjointDomains.bpl ----------------------------

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

-Execution trace:

-    DisjointDomains.bpl(11,3): start

-DisjointDomains.bpl(21,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(20,3): start

-DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains.bpl(26,3): start

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File DisjointDomains2.bpl ----------------------------

-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(9,3): start

-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(16,3): start

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

-Execution trace:

-    DisjointDomains2.bpl(30,3): start

-DisjointDomains2.bpl(39,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(37,3): start

-DisjointDomains2.bpl(49,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(45,3): start

-DisjointDomains2.bpl(63,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    DisjointDomains2.bpl(58,3): start

-

-Boogie program verifier finished with 0 verified, 6 errors

---------------------- File FunAxioms.bpl ----------------------------

-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms.bpl(18,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File FunAxioms2.bpl ----------------------------

-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    FunAxioms2.bpl(16,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File PolyList.bpl ----------------------------

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

-Execution trace:

-    PolyList.bpl(27,7): anon0

-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    PolyList.bpl(49,7): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File Maps0.bpl ----------------------------

-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(14,3): anon0

-Maps0.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(32,3): anon0

-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps0.bpl(41,9): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Maps1.bpl ----------------------------

-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Maps1.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples0.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples1.bpl ----------------------------

-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples1.bpl(13,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File InterestingExamples2.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File InterestingExamples3.bpl ----------------------------

-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples3.bpl(13,2): anon0

-

-Boogie program verifier finished with 2 verified, 1 error

---------------------- File InterestingExamples4.bpl ----------------------------

-InterestingExamples4.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterestingExamples4.bpl(36,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File InterestingExamples5.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Colors.bpl ----------------------------

-Colors.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(12,3): anon0

-Colors.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Colors.bpl(19,3): anon0

-

-Boogie program verifier finished with 0 verified, 2 errors

---------------------- File HeapAbstraction.bpl ----------------------------

-HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAbstraction.bpl(14,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File HeapAxiom.bpl ----------------------------

-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    HeapAxiom.bpl(13,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Triggers0.bpl ----------------------------

-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers0.bpl(39,3): anon0

-

-Boogie program verifier finished with 1 verified, 2 errors

---------------------- File Triggers1.bpl ----------------------------

-Triggers1.bpl(16,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Triggers1.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Keywords.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

---------------------- File Casts.bpl ----------------------------

-Casts.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Casts.bpl(6,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File BooleanQuantification.bpl ----------------------------

-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(18,3): anon0

-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification.bpl(29,3): anon0

-

-Boogie program verifier finished with 2 verified, 2 errors

---------------------- File EmptyList.bpl ----------------------------

-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int

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

-Execution trace:

-    EmptyList.bpl(26,5): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Boxing.bpl ----------------------------

-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Boxing.bpl(15,6): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapOutputTypeParams.bpl ----------------------------

-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int

-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(7,9): anon0

-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(19,9): anon0

-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapOutputTypeParams.bpl(28,8): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File ParallelAssignment.bpl ----------------------------

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

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(15,5): anon0

-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ParallelAssignment.bpl(40,11): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File BooleanQuantification2.bpl ----------------------------

-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    BooleanQuantification2.bpl(10,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Flattening.bpl ----------------------------

-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Flattening.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings.bpl ----------------------------

-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings.bpl(9,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

---------------------- File Orderings2.bpl ----------------------------

-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings2.bpl(12,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Orderings3.bpl ----------------------------

-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(15,3): anon0

-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings3.bpl(34,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

---------------------- File Orderings4.bpl ----------------------------

-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Orderings4.bpl(9,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File EmptySetBug.bpl ----------------------------

-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    EmptySetBug.bpl(25,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File Coercions2.bpl ----------------------------

-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int

-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Coercions2.bpl(18,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File MapAxiomsConsistency.bpl ----------------------------

-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.

-Execution trace:

-    MapAxiomsConsistency.bpl(79,13): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LargeLiterals0.bpl ----------------------------

-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    LargeLiterals0.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

---------------------- File LetSorting.bpl ----------------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/test7/Output b/Test/test7/Output
deleted file mode 100644
index 82c84446..00000000
--- a/Test/test7/Output
+++ /dev/null
@@ -1,64 +0,0 @@
------------------------------- NestedVC.bpl ---------------------

-NestedVC.bpl(15,4): Error BP5001: This assertion might not hold.

-Execution trace:

-    NestedVC.bpl(14,1): A

-    NestedVC.bpl(15,1): B

-

-Boogie program verifier finished with 1 verified, 1 error

------------------------------- UnreachableBlocks.bpl ---------------------

-

-Boogie program verifier finished with 4 verified, 0 errors

------------------------------- MultipleErrors.bpl ---------------------

-

------ /vc:block

-MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(3,1): start

-    MultipleErrors.bpl(6,1): A

-

-Boogie program verifier finished with 0 verified, 1 error

-

------ /vc:local

-MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(10,1): B

-

-Boogie program verifier finished with 0 verified, 1 error

-

------ /vc:dag

-MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(3,1): start

-    MultipleErrors.bpl(6,1): A

-

-Boogie program verifier finished with 0 verified, 1 error

-

------ /errorLimit:10 /vc:local

-MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(6,1): A

-MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(10,1): B

-MultipleErrors.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(14,1): C

-

-Boogie program verifier finished with 0 verified, 3 errors

-

------ /errorLimit:10 /vc:dag

-MultipleErrors.bpl(7,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(3,1): start

-    MultipleErrors.bpl(6,1): A

-MultipleErrors.bpl(11,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(3,1): start

-    MultipleErrors.bpl(10,1): B

-MultipleErrors.bpl(15,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    MultipleErrors.bpl(3,1): start

-    MultipleErrors.bpl(6,1): A

-    MultipleErrors.bpl(14,1): C

-

-Boogie program verifier finished with 0 verified, 3 errors

diff --git a/Test/textbook/Output b/Test/textbook/Output
deleted file mode 100644
index 9e2227dc..00000000
--- a/Test/textbook/Output
+++ /dev/null
@@ -1,12 +0,0 @@
-

------------------------------- Find.bpl ---------------------

-

-Boogie program verifier finished with 2 verified, 0 errors

-

------------------------------- DutchFlag.bpl ---------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

-

------------------------------- Bubble.bpl ---------------------

-

-Boogie program verifier finished with 1 verified, 0 errors