path: root/Test/dafny0/Answer

-------------------- 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;
      }
      t, u, v := M(true, lotsaObjects);
      var to: MyClass<T,U>;
      to, u, v := this.M(true, lotsaObjects);
      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(bool, myName: set<int>, int, WildData) | More(List<int>);

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

Dafny program verifier finished with 0 verified, 0 errors

-------------------- TypeTests.dfy --------------------
TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
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,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)
TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)
TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
34 resolution/type errors detected in TypeTests.dfy

-------------------- NatTypes.dfy --------------------
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon0
NatTypes.dfy(31,10): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon0
    NatTypes.dfy(19,3): anon10_LoopHead
    (0,0): anon10_LoopBody
    NatTypes.dfy(19,3): anon11_Else
    (0,0): anon3
    (0,0): anon12_Then
    (0,0): anon9
NatTypes.dfy(38,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon4_Then
NatTypes.dfy(40,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon4_Then
NatTypes.dfy(57,16): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
NatTypes.dfy(71,16): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
    (0,0): anon6_Then
NatTypes.dfy(89,19): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon6_Else
    (0,0): anon7_Else
    (0,0): anon8_Then
NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon3_Then

Dafny program verifier finished with 15 verified, 9 errors

-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
Execution trace:
    (0,0): anon0
SmallTests.dfy(61,36): Error: possible division by zero
Execution trace:
    (0,0): anon12_Then
SmallTests.dfy(62,51): Error: possible division by zero
Execution trace:
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Else
SmallTests.dfy(63,22): Error: target object may be null
Execution trace:
    (0,0): anon12_Then
    (0,0): anon3
    (0,0): anon13_Then
    (0,0): anon6
SmallTests.dfy(82,24): Error: target object may be null
Execution trace:
    (0,0): anon0
    SmallTests.dfy(81,5): anon9_LoopHead
    (0,0): anon9_LoopBody
    (0,0): anon10_Then
SmallTests.dfy(116,5): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon3
SmallTests.dfy(129,9): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
SmallTests.dfy(131,9): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(171,9): Error: assignment may update an object field not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon22_Else
    (0,0): anon5
    (0,0): anon24_Else
    (0,0): anon11
    (0,0): anon26_Else
    (0,0): anon16
    (0,0): anon28_Then
    (0,0): anon29_Then
    (0,0): anon19
SmallTests.dfy(199,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon12_Then
SmallTests.dfy(206,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Then
SmallTests.dfy(226,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Else
    (0,0): anon6
    (0,0): anon14_Then
    (0,0): anon11
SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.
SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.
Execution trace:
    (0,0): anon0
    SmallTests.dfy(266,19): anon3_Else
    (0,0): anon2
SmallTests.dfy(366,12): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(376,12): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon18_Else
    (0,0): anon11
    (0,0): anon23_Then
    (0,0): anon24_Then
    (0,0): anon15
    (0,0): anon25_Else
SmallTests.dfy(347,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon8_Then
    (0,0): anon7
SmallTests.dfy(354,10): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 47 verified, 18 errors

-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
Execution trace:
    (0,0): anon3_Else
Definedness.dfy(15,16): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(24,16): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(25,21): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
Definedness.dfy(26,17): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(33,16): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(50,18): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(51,3): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(50,22): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
Definedness.dfy(57,18): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(58,3): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(57,22): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
Definedness.dfy(65,3): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(64,22): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
Definedness.dfy(85,7): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
Definedness.dfy(86,10): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(87,10): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
Definedness.dfy(92,14): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(92,23): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(93,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(98,12): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(105,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(105,5): anon8_LoopHead
    (0,0): anon8_LoopBody
    Definedness.dfy(105,5): anon9_Else
    (0,0): anon3
Definedness.dfy(114,23): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(113,5): anon13_LoopHead
    (0,0): anon13_LoopBody
    (0,0): anon14_Then
Definedness.dfy(120,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(113,5): anon13_LoopHead
    (0,0): anon13_LoopBody
    Definedness.dfy(113,5): anon14_Else
    (0,0): anon3
    (0,0): anon15_Then
    (0,0): anon6
    Definedness.dfy(119,5): anon16_LoopHead
    (0,0): anon16_LoopBody
    (0,0): anon17_Then
Definedness.dfy(130,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(129,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    (0,0): anon0
Definedness.dfy(131,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(129,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(140,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(140,5): anon9_LoopHead
    (0,0): anon9_LoopBody
    Definedness.dfy(140,5): anon10_Else
    (0,0): anon3
Definedness.dfy(159,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(153,5): anon17_LoopHead
    (0,0): anon17_LoopBody
    Definedness.dfy(153,5): anon18_Else
    (0,0): anon3
    (0,0): anon19_Then
    (0,0): anon5
    (0,0): anon20_Then
    (0,0): anon8
    Definedness.dfy(159,5): anon21_LoopHead
    (0,0): anon21_LoopBody
    Definedness.dfy(159,5): anon22_Else
    (0,0): anon11
Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    (0,0): anon0
Definedness.dfy(178,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(170,5): anon19_LoopHead
    (0,0): anon19_LoopBody
    Definedness.dfy(170,5): anon20_Else
    (0,0): anon3
    (0,0): anon21_Then
    (0,0): anon6
    Definedness.dfy(177,5): anon22_LoopHead
    (0,0): anon22_LoopBody
    (0,0): anon23_Then
    (0,0): anon24_Then
    (0,0): anon11
Definedness.dfy(193,19): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(191,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    (0,0): anon0
Definedness.dfy(193,28): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(191,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(214,46): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
Definedness.dfy(221,22): Error: target object may be null
Execution trace:
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Definedness.dfy(237,24): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon7_Then
    (0,0): anon2
    (0,0): anon8_Else

Dafny program verifier finished with 22 verified, 36 errors

-------------------- FunctionSpecifications.dfy --------------------
FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon10_Else
    (0,0): anon11_Else
    (0,0): anon12_Then
    (0,0): anon13_Else
    (0,0): anon7
    (0,0): anon9
FunctionSpecifications.dfy(37,24): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon12_Else
    (0,0): anon15_Else
    (0,0): anon16_Then
    (0,0): anon11
FunctionSpecifications.dfy(50,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
    (0,0): anon3

Dafny program verifier finished with 3 verified, 3 errors

-------------------- ResolutionErrors.dfy --------------------
ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(261,2): Error: duplicate label
ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
45 resolution/type errors detected in ResolutionErrors.dfy

-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
8 parse errors detected in ParseErrors.dfy

-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(17,16): Error: target object may be null
Execution trace:
    (0,0): anon0
Array.dfy(24,6): Error: index out of range
Execution trace:
    (0,0): anon0
Array.dfy(48,20): Error: assertion violation
Execution trace:
    (0,0): anon0
Array.dfy(56,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(107,21): Error: upper bound below lower bound or above length of array
Execution trace:
    (0,0): anon0
    (0,0): anon14_Else
    (0,0): anon18_Then
    (0,0): anon19_Then
    (0,0): anon20_Then
    (0,0): anon11
Array.dfy(117,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
    (0,0): anon9_Else
    (0,0): anon10_Then
    (0,0): anon11_Then
    (0,0): anon12_Then
Array.dfy(119,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
    (0,0): anon9_Else
    (0,0): anon10_Then
    (0,0): anon11_Then
    (0,0): anon12_Else
Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
    (0,0): anon9_Else
    (0,0): anon10_Then
    (0,0): anon11_Then
    (0,0): anon12_Else
Array.dfy(121,8): Error: insufficient reads clause to read the indicated range of array elements
Execution trace:
    (0,0): anon9_Else
    (0,0): anon10_Then
    (0,0): anon11_Then
    (0,0): anon12_Else
Array.dfy(147,6): Error: insufficient reads clause to read array element
Execution trace:
    (0,0): anon7_Else
    (0,0): anon8_Then
    (0,0): anon9_Then
Array.dfy(155,6): Error: insufficient reads clause to read array element
Execution trace:
    (0,0): anon7_Else
    (0,0): anon8_Then
    (0,0): anon9_Then
Array.dfy(171,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
Array.dfy(178,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
Array.dfy(203,1): Error BP5003: A postcondition might not hold on this return path.
Array.dfy(202,11): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
Array.dfy(227,1): Error BP5003: A postcondition might not hold on this return path.
Array.dfy(226,11): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
Array.dfy(233,1): Error BP5003: A postcondition might not hold on this return path.
Array.dfy(232,11): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
Array.dfy(248,10): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(249,5): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then

Dafny program verifier finished with 34 verified, 20 errors

-------------------- MultiDimArray.dfy --------------------
MultiDimArray.dfy(53,21): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then
    (0,0): anon12_Then
MultiDimArray.dfy(80,25): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon6_Then

Dafny program verifier finished with 8 verified, 2 errors

-------------------- NonGhostQuantifiers.dfy --------------------
NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
11 resolution/type errors detected in NonGhostQuantifiers.dfy

-------------------- AdvancedLHS.dfy --------------------
AdvancedLHS.dfy(32,23): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon15_Else

Dafny program verifier finished with 7 verified, 1 error

-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
Modules0.dfy(72,9): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,6): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
Modules0.dfy(116,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts
Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts
Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context
Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context
13 resolution/type errors detected in Modules0.dfy

-------------------- Modules1.dfy --------------------
Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0
Execution trace:
    (0,0): anon0
Modules1.dfy(58,3): Error: failure to decrease termination measure
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 16 verified, 2 errors

-------------------- BadFunction.dfy --------------------
BadFunction.dfy(6,3): Error: failure to decrease termination measure
Execution trace:
    (0,0): anon3_Else

Dafny program verifier finished with 2 verified, 1 error

-------------------- Comprehensions.dfy --------------------
Comprehensions.dfy(9,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
    (0,0): anon10_Then
    (0,0): anon4
    (0,0): anon11_Then
    (0,0): anon12_Then
    (0,0): anon8

Dafny program verifier finished with 6 verified, 1 error

-------------------- Basics.dfy --------------------
Basics.dfy(42,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
Basics.dfy(66,42): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon13_Then
    (0,0): anon14_Then
    (0,0): anon15_Then
    Basics.dfy(66,72): anon16_Else
    (0,0): anon8
    Basics.dfy(66,82): anon17_Else
    (0,0): anon10
    Basics.dfy(66,95): anon18_Else
    (0,0): anon12
Basics.dfy(100,16): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon10_Then
Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon3
    (0,0): anon11_Else
    (0,0): anon6
    (0,0): anon12_Then
Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon10_Then
    (0,0): anon3
    (0,0): anon11_Then
    (0,0): anon6
    (0,0): anon12_Then
    (0,0): anon9
Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
    (0,0): anon0
Basics.dfy(145,19): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then
Basics.dfy(147,10): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon3
Basics.dfy(147,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3
Basics.dfy(152,12): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then
    (0,0): anon3
    (0,0): anon12_Then
Basics.dfy(163,15): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then
    (0,0): anon3
    (0,0): anon12_Else
    (0,0): anon6
    (0,0): anon13_Then
    (0,0): anon8
    (0,0): anon14_Then

Dafny program verifier finished with 19 verified, 11 errors

-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
Execution trace:
    (0,0): anon0
    (0,0): anon6_Else
    (0,0): anon7_Else
    (0,0): anon8_Else
    (0,0): anon9_Then
ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
Execution trace:
    (0,0): anon0
    (0,0): anon6_Else
    (0,0): anon7_Else
    (0,0): anon8_Then
ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
Execution trace:
    (0,0): anon0
    (0,0): anon6_Else
    (0,0): anon7_Else
    (0,0): anon8_Then
ControlStructures.dfy(43,5): Error: missing case in case statement: Red
Execution trace:
    (0,0): anon0
    (0,0): anon8_Then
    (0,0): anon9_Else
    (0,0): anon10_Then
ControlStructures.dfy(51,3): Error: missing case in case statement: Red
Execution trace:
    (0,0): anon8_Else
    (0,0): anon9_Else
    (0,0): anon10_Else
    (0,0): anon11_Else
    (0,0): anon12_Then
ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibilties
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
ControlStructures.dfy(215,18): Error: assertion violation
Execution trace:
    (0,0): anon0
    ControlStructures.dfy(194,3): anon62_LoopHead
    (0,0): anon62_LoopBody
    ControlStructures.dfy(194,3): anon63_Else
    (0,0): anon3
    ControlStructures.dfy(194,3): anon64_Else
    (0,0): anon5
    ControlStructures.dfy(198,5): anon65_LoopHead
    (0,0): anon65_LoopBody
    ControlStructures.dfy(198,5): anon66_Else
    (0,0): anon8
    ControlStructures.dfy(198,5): anon67_Else
    (0,0): anon10
    (0,0): anon71_Then
    ControlStructures.dfy(210,9): anon72_LoopHead
    (0,0): anon72_LoopBody
    ControlStructures.dfy(210,9): anon73_Else
    (0,0): anon20
    (0,0): anon74_Then
    (0,0): anon29
ControlStructures.dfy(232,21): Error: assertion violation
Execution trace:
    (0,0): anon0
    ControlStructures.dfy(194,3): anon62_LoopHead
    (0,0): anon62_LoopBody
    ControlStructures.dfy(194,3): anon63_Else
    (0,0): anon3
    ControlStructures.dfy(194,3): anon64_Else
    (0,0): anon5
    ControlStructures.dfy(198,5): anon65_LoopHead
    (0,0): anon65_LoopBody
    ControlStructures.dfy(198,5): anon66_Else
    (0,0): anon8
    ControlStructures.dfy(198,5): anon67_Else
    (0,0): anon10
    (0,0): anon71_Then
    ControlStructures.dfy(210,9): anon72_LoopHead
    (0,0): anon72_LoopBody
    ControlStructures.dfy(210,9): anon73_Else
    (0,0): anon20
    ControlStructures.dfy(210,9): anon74_Else
    (0,0): anon22
    (0,0): anon75_Then
    (0,0): after_4
    ControlStructures.dfy(221,7): anon77_LoopHead
    (0,0): anon77_LoopBody
    ControlStructures.dfy(221,7): anon78_Else
    (0,0): anon33
    ControlStructures.dfy(221,7): anon79_Else
    (0,0): anon35
    (0,0): anon81_Then
    (0,0): anon38
    (0,0): after_9
    (0,0): anon86_Then
    (0,0): anon53
ControlStructures.dfy(235,30): Error: assertion violation
Execution trace:
    (0,0): anon0
    ControlStructures.dfy(194,3): anon62_LoopHead
    (0,0): anon62_LoopBody
    ControlStructures.dfy(194,3): anon63_Else
    (0,0): anon3
    ControlStructures.dfy(194,3): anon64_Else
    (0,0): anon5
    ControlStructures.dfy(198,5): anon65_LoopHead
    (0,0): anon65_LoopBody
    ControlStructures.dfy(198,5): anon66_Else
    (0,0): anon8
    ControlStructures.dfy(198,5): anon67_Else
    (0,0): anon10
    (0,0): anon68_Then
    (0,0): after_5
    (0,0): anon87_Then
    (0,0): anon88_Then
    (0,0): anon58
ControlStructures.dfy(238,17): Error: assertion violation
Execution trace:
    (0,0): anon0
    ControlStructures.dfy(194,3): anon62_LoopHead
    (0,0): anon62_LoopBody
    ControlStructures.dfy(194,3): anon63_Else
    (0,0): anon3
    ControlStructures.dfy(194,3): anon64_Else
    (0,0): anon5
    ControlStructures.dfy(198,5): anon65_LoopHead
    (0,0): anon65_LoopBody
    ControlStructures.dfy(198,5): anon66_Else
    (0,0): anon8
    ControlStructures.dfy(198,5): anon67_Else
    (0,0): anon10
    (0,0): anon71_Then
    ControlStructures.dfy(210,9): anon72_LoopHead
    (0,0): anon72_LoopBody
    ControlStructures.dfy(210,9): anon73_Else
    (0,0): anon20
    ControlStructures.dfy(210,9): anon74_Else
    (0,0): anon22
    (0,0): anon75_Then
    (0,0): after_4
    ControlStructures.dfy(221,7): anon77_LoopHead
    (0,0): anon77_LoopBody
    ControlStructures.dfy(221,7): anon78_Else
    (0,0): anon33
    ControlStructures.dfy(221,7): anon79_Else
    (0,0): anon35
    (0,0): anon82_Then
    (0,0): anon85_Then
    (0,0): after_8
    (0,0): anon89_Then
    (0,0): anon61

Dafny program verifier finished with 18 verified, 10 errors

-------------------- Termination.dfy --------------------
Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
    (0,0): anon0
    Termination.dfy(105,3): anon7_LoopHead
    (0,0): anon7_LoopBody
    Termination.dfy(105,3): anon8_Else
    (0,0): anon3
    Termination.dfy(105,3): anon9_Else
    (0,0): anon5
Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
    (0,0): anon0
    Termination.dfy(113,3): anon9_LoopHead
    (0,0): anon9_LoopBody
    Termination.dfy(113,3): anon10_Else
    (0,0): anon11_Then
    (0,0): anon5
    Termination.dfy(113,3): anon12_Else
    (0,0): anon7
Termination.dfy(122,3): Error: decreases expression might not decrease
Execution trace:
    (0,0): anon0
    Termination.dfy(122,3): anon9_LoopHead
    (0,0): anon9_LoopBody
    Termination.dfy(122,3): anon10_Else
    (0,0): anon11_Then
    (0,0): anon5
    Termination.dfy(122,3): anon12_Else
    (0,0): anon7
Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
    (0,0): anon0
    Termination.dfy(122,3): anon9_LoopHead
    (0,0): anon9_LoopBody
    Termination.dfy(122,3): anon10_Else
    (0,0): anon11_Then
    (0,0): anon5
    Termination.dfy(122,3): anon12_Else
    (0,0): anon7
Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon6_Else
    (0,0): anon7_Else
    (0,0): anon8_Then
Termination.dfy(291,3): Error: decreases expression might not decrease
Execution trace:
    (0,0): anon0
    Termination.dfy(291,3): anon10_LoopHead
    (0,0): anon10_LoopBody
    Termination.dfy(291,3): anon11_Else
    Termination.dfy(291,3): anon12_Else
    (0,0): anon13_Else
    (0,0): anon8

Dafny program verifier finished with 45 verified, 6 errors

-------------------- DTypes.dfy --------------------
DTypes.dfy(15,14): Error: assertion violation
Execution trace:
    (0,0): anon0
DTypes.dfy(53,18): Error: assertion violation
Execution trace:
    (0,0): anon0
DTypes.dfy(117,13): Error: assertion violation
DTypes.dfy(89,30): Related location: Related location
Execution trace:
    (0,0): anon0
DTypes.dfy(123,13): Error: assertion violation
DTypes.dfy(89,20): Related location: Related location
Execution trace:
    (0,0): anon0
DTypes.dfy(133,12): Error: assertion violation
DTypes.dfy(128,6): Related location: Related location
DTypes.dfy(89,20): Related location: Related location
Execution trace:
    (0,0): anon0
DTypes.dfy(154,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon6_Then
    (0,0): anon4

Dafny program verifier finished with 27 verified, 6 errors

-------------------- ParallelResolveErrors.dfy --------------------
ParallelResolveErrors.dfy(8,6): Error: LHS of assignment must denote a mutable variable or field
ParallelResolveErrors.dfy(13,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement
ParallelResolveErrors.dfy(31,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ParallelResolveErrors.dfy(43,13): Error: set choose operator not supported inside parallel statement
ParallelResolveErrors.dfy(48,13): Error: new allocation not supported in parallel statements
ParallelResolveErrors.dfy(53,13): Error: new allocation not supported in parallel statements
ParallelResolveErrors.dfy(60,19): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(64,18): Error: return statement is not allowed inside a parallel statement
ParallelResolveErrors.dfy(71,21): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(72,20): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(73,20): Error: break label is undefined or not in scope: OutsideLoop
ParallelResolveErrors.dfy(82,24): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(83,24): Error: break label is undefined or not in scope: OutsideLoop
ParallelResolveErrors.dfy(94,43): Error: fresh expressions are not allowed in this context
ParallelResolveErrors.dfy(101,50): Error: old expressions are not allowed in this context
ParallelResolveErrors.dfy(124,12): Error: old expressions are not allowed in this context
ParallelResolveErrors.dfy(144,45): Error: fresh expressions are not allowed in this context
17 resolution/type errors detected in ParallelResolveErrors.dfy

-------------------- Parallel.dfy --------------------
Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.
Parallel.dfy(57,14): Related location: This is the precondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon29_Else
    (0,0): anon7
    (0,0): anon32_Else
    (0,0): anon10
    (0,0): anon33_Then
    (0,0): anon34_Then
    (0,0): anon35_Then
    (0,0): anon14
Parallel.dfy(35,5): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon29_Else
    (0,0): anon7
    (0,0): anon32_Else
    (0,0): anon10
    (0,0): anon33_Else
    (0,0): anon16
    (0,0): anon36_Then
    (0,0): anon37_Then
    (0,0): anon38_Then
    (0,0): anon20
Parallel.dfy(39,18): Error: possible violation of postcondition of parallel statement
Execution trace:
    (0,0): anon0
    (0,0): anon29_Else
    (0,0): anon7
    (0,0): anon32_Else
    (0,0): anon10
    (0,0): anon33_Else
    (0,0): anon16
    (0,0): anon36_Else
    (0,0): anon22
    (0,0): anon39_Then
    (0,0): anon40_Then
    (0,0): anon26
Parallel.dfy(44,19): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon29_Else
    (0,0): anon7
    (0,0): anon32_Else
    (0,0): anon10
    (0,0): anon33_Else
    (0,0): anon16
    (0,0): anon36_Else
    (0,0): anon22
    (0,0): anon39_Then
    (0,0): anon40_Then
Parallel.dfy(90,19): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon10_Else
    (0,0): anon3
    (0,0): anon11_Then
Parallel.dfy(96,20): Error: possible violation of postcondition of parallel statement
Execution trace:
    (0,0): anon0
    (0,0): anon10_Else
    (0,0): anon3
    (0,0): anon11_Then
    (0,0): anon12_Then
Parallel.dfy(119,12): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon0
    (0,0): anon6_Then
    (0,0): anon7_Then
    (0,0): anon3
Parallel.dfy(182,12): Error: left-hand sides for different parallel-statement bound variables may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon19_Then
    (0,0): anon20_Then
    (0,0): anon5

Dafny program verifier finished with 24 verified, 8 errors

-------------------- TypeParameters.dfy --------------------
TypeParameters.dfy(44,22): Error: assertion violation
Execution trace:
    (0,0): anon0
TypeParameters.dfy(66,27): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
    (0,0): anon2
TypeParameters.dfy(138,12): Error: assertion violation
TypeParameters.dfy(138,28): Related location: Related location
Execution trace:
    (0,0): anon0
    (0,0): anon14_Then
    TypeParameters.dfy(138,32): anon15_Else
    (0,0): anon5
TypeParameters.dfy(140,12): Error: assertion violation
TypeParameters.dfy(140,33): Related location: Related location
Execution trace:
    (0,0): anon0
    (0,0): anon17_Then
    TypeParameters.dfy(140,37): anon18_Else
    (0,0): anon11
TypeParameters.dfy(154,15): Error BP5005: This loop invariant might not be maintained by the loop.
TypeParameters.dfy(154,38): Related location: Related location
Execution trace:
    (0,0): anon0
    TypeParameters.dfy(147,3): anon17_LoopHead
    (0,0): anon17_LoopBody
    TypeParameters.dfy(147,3): anon18_Else
    (0,0): anon5
    (0,0): anon20_Then
    (0,0): anon8
    TypeParameters.dfy(153,3): anon21_LoopHead
    (0,0): anon21_LoopBody
    TypeParameters.dfy(153,3): anon22_Else
    (0,0): anon13
    TypeParameters.dfy(153,3): anon24_Else
    (0,0): anon15

Dafny program verifier finished with 35 verified, 5 errors

-------------------- Datatypes.dfy --------------------
Datatypes.dfy(79,20): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon20_Else
    (0,0): anon21_Then
    (0,0): anon4
    (0,0): anon22_Else
    (0,0): anon23_Then
    (0,0): anon24_Else
    (0,0): anon25_Then
Datatypes.dfy(167,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon4_Then
Datatypes.dfy(169,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon5_Then
Datatypes.dfy(198,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
Execution trace:
    (0,0): anon0
Datatypes.dfy(201,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
Execution trace:
    (0,0): anon0
    (0,0): anon6_Then

Dafny program verifier finished with 29 verified, 5 errors

-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
Execution trace:
    (0,0): anon0
TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this return path.
TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon25_Then
    (0,0): anon6
    (0,0): anon28_Then
    (0,0): anon8
    (0,0): anon29_Else
    (0,0): anon13
    (0,0): anon31_Else
    (0,0): anon18
    (0,0): anon33_Then
    (0,0): anon20
    (0,0): anon34_Then
    (0,0): anon35_Then
    (0,0): anon24
TypeAntecedents.dfy(63,16): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon25_Else
    (0,0): anon26_Then
    (0,0): anon27_Else

Dafny program verifier finished with 12 verified, 3 errors

-------------------- SplitExpr.dfy --------------------

Dafny program verifier finished with 5 verified, 0 errors

-------------------- Refinement.dfy --------------------

Dafny program verifier finished with 53 verified, 0 errors

-------------------- RefinementErrors.dfy --------------------
RefinementErrors.dfy(1,6): Error: Detected a cyclic refinement declaration: C -> B -> A
RefinementErrors.dfy(27,11): Error: Coupling invariants can only be declared in refinement classes
RefinementErrors.dfy(40,6): Error: Refined class has a member with the same name as in the refinement class: x
RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name as in the refinement class: M
RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M
RefinementErrors.dfy(34,10): Error: Different number of output variables
6 resolution/type errors detected in RefinementErrors.dfy

-------------------- LoopModifies.dfy --------------------
LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(14,4): anon9_LoopHead
    (0,0): anon9_LoopBody
    LoopModifies.dfy(14,4): anon10_Else
    (0,0): anon5
    LoopModifies.dfy(14,4): anon12_Else
    (0,0): anon7
LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(42,4): anon9_LoopHead
    (0,0): anon9_LoopBody
    LoopModifies.dfy(42,4): anon10_Else
    (0,0): anon5
    LoopModifies.dfy(42,4): anon12_Else
    (0,0): anon7
LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(57,4): anon9_LoopHead
    (0,0): anon9_LoopBody
    LoopModifies.dfy(57,4): anon10_Else
    (0,0): anon5
    LoopModifies.dfy(57,4): anon12_Else
    (0,0): anon7
LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
Execution trace:
    (0,0): anon0
LoopModifies.dfy(98,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(90,4): anon9_LoopHead
    (0,0): anon9_LoopBody
    LoopModifies.dfy(90,4): anon10_Else
    (0,0): anon5
    LoopModifies.dfy(90,4): anon12_Else
    (0,0): anon7
LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(134,4): anon17_LoopHead
    (0,0): anon17_LoopBody
    LoopModifies.dfy(134,4): anon18_Else
    (0,0): anon5
    LoopModifies.dfy(134,4): anon20_Else
    (0,0): anon7
    LoopModifies.dfy(139,7): anon21_LoopHead
    (0,0): anon21_LoopBody
    LoopModifies.dfy(139,7): anon22_Else
    (0,0): anon12
    LoopModifies.dfy(139,7): anon24_Else
    (0,0): anon14
LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(193,4): anon9_LoopHead
    (0,0): anon9_LoopBody
    LoopModifies.dfy(193,4): anon10_Else
    (0,0): anon5
    LoopModifies.dfy(193,4): anon12_Else
    (0,0): anon7
LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    LoopModifies.dfy(273,4): anon17_LoopHead
    (0,0): anon17_LoopBody
    LoopModifies.dfy(273,4): anon18_Else
    (0,0): anon5
    LoopModifies.dfy(273,4): anon20_Else
    (0,0): anon7
    LoopModifies.dfy(281,7): anon21_LoopHead
    (0,0): anon21_LoopBody
    LoopModifies.dfy(281,7): anon22_Else
    (0,0): anon12
    LoopModifies.dfy(281,7): anon24_Else
    (0,0): anon14

Dafny program verifier finished with 23 verified, 9 errors

-------------------- ReturnErrors.dfy --------------------
ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.
3 resolution/type errors detected in ReturnErrors.dfy

-------------------- ReturnTests.dfy --------------------

Dafny program verifier finished with 16 verified, 0 errors

-------------------- ChainingDisjointTests.dfy --------------------

Dafny program verifier finished with 6 verified, 0 errors

-------------------- CallStmtTests.dfy --------------------
CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy

-------------------- MultiSets.dfy --------------------

Dafny program verifier finished with 22 verified, 0 errors

-------------------- PredExpr.dfy --------------------
PredExpr.dfy(4,12): Error: condition in assert expression might not hold
Execution trace:
    (0,0): anon3_Else
PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative
Execution trace:
    (0,0): anon6_Else
    (0,0): anon7_Else
PredExpr.dfy(49,17): Error: condition in assert expression might not hold
Execution trace:
    (0,0): anon0
PredExpr.dfy(74,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon8_Else
    (0,0): anon3
    PredExpr.dfy(73,20): anon10_Else
    (0,0): anon6

Dafny program verifier finished with 11 verified, 4 errors

-------------------- LetExpr.dfy --------------------
LetExpr.dfy(5,12): Error: assertion violation
Execution trace:
    (0,0): anon0
LetExpr.dfy(104,21): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then

Dafny program verifier finished with 13 verified, 2 errors