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

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, 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)
      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
    }
  }

  function F(x: int, y: int, h: WildData, k: WildData): WildData
  {
    if x < 0 then
      h
    else if x == 0 then
      if if h == k then true else false then
        h
      else if y == 0 then
        k
      else
        h
    else
      k
  }
}

datatype List<T> {
  Nil;
  Cons(T, List<T>);
}

datatype WildData {
  Something;
  JustAboutAnything<G, H>(G, myName: set<H>, int, WildData);
  More(List<int>);
}

class C {
  var w: WildData;
  var list: List<bool>;
}

Dafny program verifier finished with 0 verified, 0 errors

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

Boogie program verifier finished with 8 verified, 0 errors

-------------------- TypeTests.dfy --------------------
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
9 resolution/type errors detected in TypeTests.dfy

-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,7): Error: RHS expression must be well defined
Execution trace:
    (0,0): anon0
SmallTests.dfy(61,36): Error: possible division by zero
Execution trace:
    (0,0): anon10_Then
SmallTests.dfy(62,51): Error: possible division by zero
Execution trace:
    (0,0): anon10_Else
    (0,0): anon3
    (0,0): anon11_Else
SmallTests.dfy(63,22): Error: target object may be null
Execution trace:
    (0,0): anon10_Then
    (0,0): anon3
    (0,0): anon11_Then
    (0,0): anon6

Dafny program verifier finished with 6 verified, 4 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 6 verified, 0 errors

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

Dafny program verifier finished with 6 verified, 0 errors

-------------------- Use.dfy --------------------
Use.dfy(15,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(26,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(35,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(56,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(88,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(130,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(152,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(170,5): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(215,5): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 20 verified, 9 errors

-------------------- DTypes.dfy --------------------
DTypes.dfy(15,5): Error: assertion violation
Execution trace:
    (0,0): anon0
DTypes.dfy(28,5): Error: assertion violation
Execution trace:
    (0,0): anon0
DTypes.dfy(54,5): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 5 verified, 3 errors

-------------------- TypeParameters.dfy --------------------
TypeParameters.dfy(41,5): Error: assertion violation
Execution trace:
    (0,0): anon0
TypeParameters.dfy(63,5): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 10 verified, 2 errors

-------------------- Datatypes.dfy --------------------

Dafny program verifier finished with 6 verified, 0 errors

-------------------- UnboundedStack.dfy --------------------

Dafny program verifier finished with 7 verified, 0 errors

-------------------- SumOfCubes.dfy --------------------

Dafny program verifier finished with 10 verified, 0 errors

-------------------- TerminationDemos.dfy --------------------

Dafny program verifier finished with 7 verified, 0 errors