Snapshot, to be continued

32 files changed, 145 insertions, 140 deletions

diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect
index 82fc2933..ab2bbc52 100644
--- a/Test/dafny0/Backticks.dfy.expect
+++ b/Test/dafny0/Backticks.dfy.expect
@@ -3,7 +3,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

-Backticks.dfy(77,7): Error: call may violate context's modifies clause

+Backticks.dfy(77,8): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect
index 57a33c62..8a334754 100644
--- a/Test/dafny0/CallStmtTests.dfy.expect
+++ b/Test/dafny0/CallStmtTests.dfy.expect
@@ -1,3 +1,3 @@
 CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable

-CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable

+CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable

 2 resolution/type errors detected in CallStmtTests.dfy

diff --git a/Test/dafny0/CoPrefix.dfy.expect b/Test/dafny0/CoPrefix.dfy.expect
index c2453a09..c92a09c1 100644
--- a/Test/dafny0/CoPrefix.dfy.expect
+++ b/Test/dafny0/CoPrefix.dfy.expect
@@ -8,17 +8,17 @@ CoPrefix.dfy(168,15): Related location: This is the postcondition that might not
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause

+CoPrefix.dfy(176,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoPrefix.dfy(63,7): Error: failure to decrease termination measure

+CoPrefix.dfy(63,57): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

     (0,0): anon8_Else

     (0,0): anon9_Then

-CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause

+CoPrefix.dfy(76,56): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect
index 9acb5a58..45d1e598 100644
--- a/Test/dafny0/CoResolution.dfy.expect
+++ b/Test/dafny0/CoResolution.dfy.expect
@@ -7,19 +7,19 @@ CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any read
 CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause

 CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(95,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates

+CoResolution.dfy(115,24): Error: a recursive call from a copredicate can go only to other copredicates

+CoResolution.dfy(121,28): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

-CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates

+CoResolution.dfy(135,26): Error: a recursive call from a copredicate can go only to other copredicates

+CoResolution.dfy(141,30): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined

-CoResolution.dfy(202,12): Error: the type of this expression is underspecified

+CoResolution.dfy(202,13): Error: the type of this expression is underspecified

 CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined

 24 resolution/type errors detected in CoResolution.dfy

diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect
index ce3e3a8d..26fec211 100644
--- a/Test/dafny0/Coinductive.dfy.expect
+++ b/Test/dafny0/Coinductive.dfy.expect
@@ -13,5 +13,5 @@ Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in
 Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates

+Coinductive.dfy(148,21): Error: a recursive call from a copredicate can go only to other copredicates

 16 resolution/type errors detected in Coinductive.dfy

diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 7869fba3..f39aa4ce 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -28,3 +28,10 @@ function F(d: Dt): Dt
 {

   d[x := 5]

 }

+

+datatype NumericNames = NumNam(010: int)

+

+method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)

+{

+  pp := nn[010 := y];  // not to be confused with a field name 10

+}

diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 52595bf9..790f6509 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 3 verified, 0 errors

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect
index f6b51252..874df45e 100644
--- a/Test/dafny0/Datatypes.dfy.expect
+++ b/Test/dafny0/Datatypes.dfy.expect
@@ -47,11 +47,11 @@ Execution trace:
     (0,0): anon23_Then

     (0,0): anon24_Else

     (0,0): anon25_Then

-Datatypes.dfy(170,14): Error: assertion violation

+Datatypes.dfy(170,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Then

-Datatypes.dfy(172,14): Error: assertion violation

+Datatypes.dfy(172,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index f296ed4b..9f277582 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by
 EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality

 EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality

 EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)

-EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)

+EqualityTypes.dfy(85,9): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)

 EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)

@@ -26,10 +26,10 @@ EqualityTypes.dfy(210,8): Error: set argument type must support equality (got Co
 EqualityTypes.dfy(211,20): Error: set argument type must support equality (got Co)

 EqualityTypes.dfy(211,29): Error: set argument type must support equality (got Co)

 EqualityTypes.dfy(212,17): Error: set argument type must support equality (got Co)

-EqualityTypes.dfy(233,4): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)

+EqualityTypes.dfy(233,12): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)

 EqualityTypes.dfy(233,13): Error: set argument type must support equality (got Co)

 EqualityTypes.dfy(234,19): Error: set argument type must support equality (got Co)

-EqualityTypes.dfy(236,4): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)

+EqualityTypes.dfy(236,34): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)

 EqualityTypes.dfy(236,35): Error: set argument type must support equality (got Co)

 EqualityTypes.dfy(238,24): Error: set argument type must support equality (got Co)

 EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)

diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index e7df68f7..4b9aa202 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -41,7 +41,7 @@ FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplyin
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(167,3): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(167,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

diff --git a/Test/dafny0/Iterators.dfy.expect b/Test/dafny0/Iterators.dfy.expect
index 0087691b..f0c6e400 100644
--- a/Test/dafny0/Iterators.dfy.expect
+++ b/Test/dafny0/Iterators.dfy.expect
@@ -1,38 +1,38 @@
-Iterators.dfy(251,9): Error: failure to decrease termination measure

+Iterators.dfy(251,10): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

-Iterators.dfy(274,9): Error: failure to decrease termination measure

+Iterators.dfy(274,10): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

-Iterators.dfy(284,24): Error: failure to decrease termination measure

+Iterators.dfy(284,32): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause

+Iterators.dfy(296,10): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

-Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause

+Iterators.dfy(317,10): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

-Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause

+Iterators.dfy(326,32): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-Iterators.dfy(343,9): Error: failure to decrease termination measure

+Iterators.dfy(343,10): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

-Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause

+Iterators.dfy(353,32): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-Iterators.dfy(370,9): Error: failure to decrease termination measure

+Iterators.dfy(370,10): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

@@ -65,7 +65,7 @@ Execution trace:
     Iterators.dfy(197,3): anon17_Else

     Iterators.dfy(197,3): anon19_Else

     (0,0): anon21_Then

-Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold.

+Iterators.dfy(40,22): Error BP5002: A precondition for this call might not hold.

 Iterators.dfy(4,10): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

@@ -85,13 +85,13 @@ Iterators.dfy(150,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

-Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold.

+Iterators.dfy(155,24): Error BP5002: A precondition for this call might not hold.

 Iterators.dfy(125,10): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Then

     (0,0): anon3

-Iterators.dfy(234,14): Error: assertion violation

+Iterators.dfy(234,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     Iterators.dfy(225,3): anon14_LoopHead

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index e50dc797..90436ed8 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -8,11 +8,11 @@ Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass
 Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down

-Modules0.dfy(76,6): Error: expected method call, found expression

+Modules0.dfy(76,13): Error: expected method call, found expression

 Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down

-Modules0.dfy(79,6): Error: expected method call, found expression

+Modules0.dfy(79,13): Error: expected method call, found expression

 Modules0.dfy(84,8): Error: type MyClassY does not have a member M

-Modules0.dfy(84,6): Error: expected method call, found expression

+Modules0.dfy(84,9): Error: expected method call, found expression

 Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

 Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)

@@ -23,12 +23,12 @@ Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did
 Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)

 Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(287,6): Error: expected method call, found expression

+Modules0.dfy(287,17): Error: expected method call, found expression

 Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point

-Modules0.dfy(288,6): Error: expected method call, found expression

+Modules0.dfy(288,17): Error: expected method call, found expression

 Modules0.dfy(310,24): Error: module Q_Imp does not exist

 Modules0.dfy(102,6): Error: type MyClassY does not have a member M

-Modules0.dfy(102,4): Error: expected method call, found expression

+Modules0.dfy(102,7): Error: expected method call, found expression

 Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts

 Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts

 Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts

diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect
index b269e3b2..342b5808 100644
--- a/Test/dafny0/Modules1.dfy.expect
+++ b/Test/dafny0/Modules1.dfy.expect
@@ -10,11 +10,11 @@ Modules1.dfy(94,18): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0

+Modules1.dfy(56,9): Error: decreases expression must be bounded below by 0

 Modules1.dfy(54,13): Related location

 Execution trace:

     (0,0): anon0

-Modules1.dfy(62,3): Error: failure to decrease termination measure

+Modules1.dfy(62,9): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect
index b0613150..7bee017c 100644
--- a/Test/dafny0/NatTypes.dfy.expect
+++ b/Test/dafny0/NatTypes.dfy.expect
@@ -25,7 +25,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(92,22): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -35,7 +35,7 @@ Execution trace:
     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

-NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(130,35): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect
index bb1624f9..28b745c5 100644
--- a/Test/dafny0/NewtypesResolution.dfy.expect
+++ b/Test/dafny0/NewtypesResolution.dfy.expect
@@ -14,14 +14,14 @@ NewtypesResolution.dfy(91,31): Error: old expressions are not allowed in this co
 NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N

 NewtypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle

 NewtypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle

-NewtypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable

+NewtypesResolution.dfy(120,21): Error: name of type (N9) is used as a variable

 NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)

 NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)

-NewtypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable

-NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable

-NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass

-NewtypesResolution.dfy(162,4): Error: expected method call, found expression

-NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

+NewtypesResolution.dfy(156,9): Error: name of type (B) is used as a variable

+NewtypesResolution.dfy(157,11): Error: name of type (Syn) is used as a variable

+NewtypesResolution.dfy(162,8): Error: member 'U' does not exist in type 'Y'

+NewtypesResolution.dfy(162,9): Error: expected method call, found expression

+NewtypesResolution.dfy(188,60): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

 NewtypesResolution.dfy(219,11): Error: new must use an integer-based expression for the array size (got real for index 2)

 NewtypesResolution.dfy(221,13): Error: arguments to < must have the same type (got Even and nat)

 NewtypesResolution.dfy(223,13): Error: arguments to < must have the same type (got Even and int)

diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect
index df076f60..3aa09714 100644
--- a/Test/dafny0/OpaqueFunctions.dfy.expect
+++ b/Test/dafny0/OpaqueFunctions.dfy.expect
@@ -1,30 +1,30 @@
 OpaqueFunctions.dfy(27,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

-OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy(52,8): Error BP5002: A precondition for this call might not hold.

 OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

 OpaqueFunctions.dfy(58,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

-OpaqueFunctions.dfy(60,14): Error: assertion violation

+OpaqueFunctions.dfy(60,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-OpaqueFunctions.dfy(63,14): Error: assertion violation

+OpaqueFunctions.dfy(63,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Then

-OpaqueFunctions.dfy(66,14): Error: assertion violation

+OpaqueFunctions.dfy(66,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-OpaqueFunctions.dfy(77,14): Error: assertion violation

+OpaqueFunctions.dfy(77,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy(79,10): Error BP5002: A precondition for this call might not hold.

 OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

@@ -32,23 +32,23 @@ Execution trace:
 OpaqueFunctions.dfy(86,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

-OpaqueFunctions.dfy(88,14): Error: assertion violation

+OpaqueFunctions.dfy(88,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-OpaqueFunctions.dfy(91,14): Error: assertion violation

+OpaqueFunctions.dfy(91,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Then

-OpaqueFunctions.dfy(94,14): Error: assertion violation

+OpaqueFunctions.dfy(94,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-OpaqueFunctions.dfy(105,14): Error: assertion violation

+OpaqueFunctions.dfy(105,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy(107,10): Error BP5002: A precondition for this call might not hold.

 OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

@@ -56,19 +56,19 @@ Execution trace:
 OpaqueFunctions.dfy(114,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

-OpaqueFunctions.dfy(116,14): Error: assertion violation

+OpaqueFunctions.dfy(116,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-OpaqueFunctions.dfy(119,14): Error: assertion violation

+OpaqueFunctions.dfy(119,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Then

-OpaqueFunctions.dfy(122,14): Error: assertion violation

+OpaqueFunctions.dfy(122,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-OpaqueFunctions.dfy(138,12): Error: assertion violation

+OpaqueFunctions.dfy(138,13): Error: assertion violation

 Execution trace:

     (0,0): anon0

 OpaqueFunctions.dfy(202,12): Error: assertion violation

diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect
index c994cd39..6b726cd5 100644
--- a/Test/dafny0/Parallel.dfy.expect
+++ b/Test/dafny0/Parallel.dfy.expect
@@ -1,4 +1,4 @@
-Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold.

+Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.

 Parallel.dfy(60,14): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

@@ -60,7 +60,7 @@ Execution trace:
     (0,0): anon19_Then

     (0,0): anon20_Then

     (0,0): anon5

-Parallel.dfy(296,10): Error: assertion violation

+Parallel.dfy(296,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect
index 78a43ed9..7305bfce 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy.expect
+++ b/Test/dafny0/ParallelResolveErrors.dfy.expect
@@ -7,8 +7,8 @@ ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost con
 ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context

 ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context

 ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

+ParallelResolveErrors.dfy(65,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

+ParallelResolveErrors.dfy(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

 ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops

 ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement

 ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops

@@ -17,6 +17,6 @@ ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scop
 ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops

 ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop

 ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

-ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

+ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

+ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

 21 resolution/type errors detected in ParallelResolveErrors.dfy

diff --git a/Test/dafny0/RealCompare.dfy.expect b/Test/dafny0/RealCompare.dfy.expect
index e0f70fc0..5b25fa25 100644
--- a/Test/dafny0/RealCompare.dfy.expect
+++ b/Test/dafny0/RealCompare.dfy.expect
@@ -1,8 +1,8 @@
-RealCompare.dfy(35,5): Error: failure to decrease termination measure

+RealCompare.dfy(35,6): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0

+RealCompare.dfy(50,4): Error: decreases expression must be bounded below by 0.0

 RealCompare.dfy(48,13): Related location

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index bb51b01f..2f340557 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -95,8 +95,8 @@ method TestNameResolution1() {
                             // parameters match the signature of only one of those constructors)

   var d3 := Abc.David(20, 40);  // error: wrong number of parameters

   var d4 := Rst.David(20, 40);

-  var e := Eleanor;

-  assert Tuv(e, this.Eleanor) == 10;

+  var e := Eleanor;  // this resolves to the field, not the Abc datatype constructor

+  assert Tuv(Abc.Eleanor, e) == 10;

 }

 

 // --------------- ghost tests -------------------------------------

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 7789c6f8..9ba6a1b3 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -16,27 +16,27 @@ ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts
 ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts

-ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(619,29): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(621,17): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(676,18): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(686,22): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field 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(700,16): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(702,18): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause

-ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(724,22): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field 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(732,16): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations

-ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(734,9): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause

-ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression

-ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1)

+ResolutionErrors.dfy(762,17): Error: calls to methods with side-effects are not allowed inside a statement expression

+ResolutionErrors.dfy(763,18): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(764,18): Error: wrong number of method result arguments (got 0, expected 1)

 ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

 ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts

@@ -92,13 +92,13 @@ ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

 ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable

+ResolutionErrors.dfy(117,10): Error: actual out-parameter 0 is required to be a ghost variable

 ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(149,10): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

 ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

@@ -124,32 +124,31 @@ ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
 ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)

 ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)

-ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name

+ResolutionErrors.dfy(56,14): Error: accessing member 'X' requires an instance expression

 ResolutionErrors.dfy(57,7): Error: unresolved identifier: F

-ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name

-ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance

+ResolutionErrors.dfy(58,14): Error: accessing member 'F' requires an instance expression

 ResolutionErrors.dfy(59,7): Error: unresolved identifier: G

 ResolutionErrors.dfy(61,7): Error: unresolved identifier: M

-ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance

+ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance expression

 ResolutionErrors.dfy(63,7): Error: unresolved identifier: N

-ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters

-ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global

+ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters

+ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'

 ResolutionErrors.dfy(86,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(91,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: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

+ResolutionErrors.dfy(96,16): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)

 ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label

 ResolutionErrors.dfy(263,2): Error: duplicate label

 ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

 ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(292,4): Error: a constructor is allowed to be called only when an object is being allocated

+ResolutionErrors.dfy(292,9): Error: a constructor is allowed to be called only when an object is being allocated

 ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)

 ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)

 ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)

 ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts

 ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

+ResolutionErrors.dfy(345,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

 ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

 ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)

 ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)

@@ -160,7 +159,7 @@ ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(384,6): Error: print 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(406,6): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(406,9): Error: calls to methods with side-effects are not allowed inside a hint

 ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations

 ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint

 ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts

@@ -174,14 +173,13 @@ ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies cla
 ResolutionErrors.dfy(913,9): Error: unresolved identifier: s

 ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))

 ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))

-ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int

+ResolutionErrors.dfy(931,16): Error: condition is expected to be of type bool, but is int

 ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3

 ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2

-ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))

 ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)

 ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)

 ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait

 ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)

-ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

+ResolutionErrors.dfy(1129,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-186 resolution/type errors detected in ResolutionErrors.dfy

+184 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/ReturnErrors.dfy.expect b/Test/dafny0/ReturnErrors.dfy.expect
index a2b9d86d..3f43c226 100644
--- a/Test/dafny0/ReturnErrors.dfy.expect
+++ b/Test/dafny0/ReturnErrors.dfy.expect
@@ -1,4 +1,4 @@
-ReturnErrors.dfy(32,10): Error: cannot have method call in return statement.

-ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement.

+ReturnErrors.dfy(32,11): Error: cannot have method call in return statement.

+ReturnErrors.dfy(38,11): Error: cannot have effectful parameter in multi-return statement.

 ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'.

 3 resolution/type errors detected in ReturnErrors.dfy

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 824ad991..1983d2ac 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -24,16 +24,16 @@ Execution trace:
     SmallTests.dfy(84,5): anon8_LoopHead

     (0,0): anon8_LoopBody

     (0,0): anon9_Then

-SmallTests.dfy(119,5): Error: call may violate context's modifies clause

+SmallTests.dfy(119,6): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

-SmallTests.dfy(132,9): Error: call may violate context's modifies clause

+SmallTests.dfy(132,10): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-SmallTests.dfy(134,9): Error: call may violate context's modifies clause

+SmallTests.dfy(134,10): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

@@ -174,7 +174,7 @@ Execution trace:
 SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(644,10): Error: assertion violation

+SmallTests.dfy(644,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

diff --git a/Test/dafny0/StatementExpressions.dfy.expect b/Test/dafny0/StatementExpressions.dfy.expect
index 3f50d6d9..313c8884 100644
--- a/Test/dafny0/StatementExpressions.dfy.expect
+++ b/Test/dafny0/StatementExpressions.dfy.expect
@@ -1,4 +1,4 @@
-StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause

+StatementExpressions.dfy(55,12): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Then

@@ -16,7 +16,7 @@ StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negat
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause

+StatementExpressions.dfy(98,18): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Then

diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect
index dc1eec5b..5c63112a 100644
--- a/Test/dafny0/TailCalls.dfy.expect
+++ b/Test/dafny0/TailCalls.dfy.expect
@@ -1,4 +1,4 @@
-TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code

+TailCalls.dfy(21,16): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code

 TailCalls.dfy(38,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods

 TailCalls.dfy(43,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods

 3 resolution/type errors detected in TailCalls.dfy

diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index ef8ee72e..fd86c8cb 100644
--- a/Test/dafny0/Termination.dfy.expect
+++ b/Test/dafny0/Termination.dfy.expect
@@ -1,4 +1,4 @@
-Termination.dfy[TerminationRefinement1](440,5): Error: failure to decrease termination measure

+Termination.dfy[TerminationRefinement1](440,6): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

 Termination.dfy(360,47): Error: failure to decrease termination measure

diff --git a/Test/dafny0/Trait/TraitExtend.dfy.expect b/Test/dafny0/Trait/TraitExtend.dfy.expect
index 73a24ad8..2051fd81 100644
--- a/Test/dafny0/Trait/TraitExtend.dfy.expect
+++ b/Test/dafny0/Trait/TraitExtend.dfy.expect
@@ -1,3 +1,3 @@
-TraitExtend.dfy(40,20): Error: wrong number of function arguments (got 2, expected 3)

-TraitExtend.dfy(41,20): Error: wrong number of function arguments (got 3, expected 2)

+TraitExtend.dfy(40,24): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)

+TraitExtend.dfy(41,24): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)

 2 resolution/type errors detected in TraitExtend.dfy

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 55fc916c..0a15ad67 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,13 +1,13 @@
 TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

 TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

 TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)

-TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D)

-TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C)

-TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int)

-TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int)

-TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)

-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C)

-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int)

+TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)

+TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)

+TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)

+TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, got int)

+TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)

+TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)

+TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)

 TypeTests.dfy(47,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(56,6): Error: Duplicate local-variable name: z

 TypeTests.dfy(58,6): Error: Duplicate local-variable name: x

diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index eedfce29..b37633ae 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -1,14 +1,14 @@
 

 -------------------- Snapshots0.dfy --------------------

-Processing command (at Snapshots0.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

 Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

-Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,3)):

+Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):

   >>> added after: a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);

-Processing command (at Snapshots0.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

 Processing command (at <unknown location>) a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);

   >>> AssumeNegationOfAssumptionVariable

@@ -21,7 +21,7 @@ Execution trace:
 Dafny program verifier finished with 2 verified, 1 error

 

 -------------------- Snapshots1.dfy --------------------

-Processing command (at Snapshots1.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

 Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);

   >>> DoNothingToAssert

@@ -29,11 +29,11 @@ Processing command (at Snapshots1.v0.dfy(12,3)) assert true;
   >>> DoNothingToAssert

 

 Dafny program verifier finished with 4 verified, 0 errors

-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,3)):

+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):

   >>> added after: a##post##0 := a##post##0 && false;

 Processing command (at Snapshots1.v1.dfy(12,3)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots1.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);

   >>> DoNothingToAssert

@@ -44,7 +44,7 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 1 error

 

 -------------------- Snapshots2.dfy --------------------

-Processing command (at Snapshots2.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);

   >>> DoNothingToAssert

@@ -60,11 +60,11 @@ Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
   >>> DoNothingToAssert

 

 Dafny program verifier finished with 6 verified, 0 errors

-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,3)):

+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):

   >>> added after: a##post##0 := a##post##0 && false;

 Processing command (at Snapshots2.v1.dfy(18,3)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);

   >>> DoNothingToAssert

@@ -125,11 +125,11 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 2 errors

 

 -------------------- Snapshots5.dfy --------------------

-Processing command (at Snapshots5.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

   >>> DoNothingToAssert

-Processing command (at Snapshots5.v0.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

   >>> DoNothingToAssert

@@ -137,11 +137,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: tru
   >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

-Processing command (at Snapshots5.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots5.v1.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

   >>> MarkAsFullyVerified

diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect
index d84bdc45..849b9e38 100644
--- a/Test/dafny2/SnapshotableTrees.dfy.expect
+++ b/Test/dafny2/SnapshotableTrees.dfy.expect
@@ -1,4 +1,4 @@
-SnapshotableTrees.dfy(68,16): Error BP5002: A precondition for this call might not hold.

+SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold.

 SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect
index 927d8b06..9f6998f5 100644
--- a/Test/hofs/Field.dfy.expect
+++ b/Test/hofs/Field.dfy.expect
@@ -1,14 +1,14 @@
-Field.dfy(12,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

 Field.dfy(12,12): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Field.dfy(21,10): Error: assertion violation

+Field.dfy(12,15): Error: assertion violation

 Execution trace:

     (0,0): anon0

 Field.dfy(21,12): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

+Field.dfy(21,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 

 Dafny program verifier finished with 2 verified, 4 errors

diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index 2cf19369..c3e0c242 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -1,5 +1,5 @@
 ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable to LHS (of type (int,bool) -> real)

-ResolveError.dfy(91,14): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)

+ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)

 ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)

 ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)

 ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

@@ -8,12 +8,12 @@ ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field
 ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)

 ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)

 ResolveError.dfy(33,13): Error: type mismatch for argument 0 (function expects int, got bool)

-ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)

+ResolveError.dfy(34,22): Error: type mismatch for argument 0 (function expects int, got bool)

 ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)

-ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)

-ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected int, got bool)

+ResolveError.dfy(36,21): Error: wrong number of arguments to function application (function 'requires' expects 1, got 2)

+ResolveError.dfy(37,19): Error: type mismatch for argument 0 (function expects int, got bool)

 ResolveError.dfy(38,22): Error: arguments must have the same type (got set<object> and int)

-ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expected 1)

+ResolveError.dfy(39,18): Error: wrong number of arguments to function application (function 'reads' expects 1, got 2)

 ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)

 ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)

 ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool