1 files changed, 210 insertions, 163 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index c215d354..d1d826f4 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -1,102 +1,3 @@
-ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
-ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
-ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements
-ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
-ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(704,11): 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(704,11): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(736,11): 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(736,11): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(741,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)
-ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)
-ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)
-ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
-ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
-ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
-ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
-ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
-ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
-ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
-ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
-ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
-ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
-ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
-ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
-ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)
-ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)
-ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1118,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1120,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
-ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
-ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
-ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
-ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
-ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
 ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
 ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
@@ -107,31 +8,183 @@ ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specific
 ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint
-ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
-ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(446,9): Error: class Lamb does not have an anonymous constructor
-ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
-ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x
-ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(241,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(264,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(278,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(283,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(362,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(444,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(446,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(448,12): Error: a hint is not allowed to update a variable declared outside the hint
+ResolutionErrors.dfy(535,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(540,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
+ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
+ResolutionErrors.dfy(598,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(599,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(629,15): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(638,17): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(655,14): Error: new allocation not supported in forall statements
+ResolutionErrors.dfy(660,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ResolutionErrors.dfy(660,14): Error: new allocation not allowed in ghost context
+ResolutionErrors.dfy(672,21): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(712,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(745,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(776,19): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(777,20): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(789,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(799,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(810,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(819,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(833,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(834,6): Error: RHS (of type int) not assignable to LHS (of type object)
+ResolutionErrors.dfy(835,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(840,6): Error: RHS (of type G) not assignable to LHS (of type object)
+ResolutionErrors.dfy(841,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(842,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(867,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(885,20): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(896,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(912,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(913,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(918,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(919,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(920,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(921,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(922,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(923,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(1004,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
+ResolutionErrors.dfy(1005,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
+ResolutionErrors.dfy(1016,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(1013,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
+ResolutionErrors.dfy(1014,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1015,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1022,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
+ResolutionErrors.dfy(1025,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1038,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+ResolutionErrors.dfy(1041,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1046,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1065,21): Error: unresolved identifier: x
+ResolutionErrors.dfy(1072,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
+ResolutionErrors.dfy(1084,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1094,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
+ResolutionErrors.dfy(1099,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
+ResolutionErrors.dfy(1104,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
+ResolutionErrors.dfy(1105,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
+ResolutionErrors.dfy(1110,13): Error: arguments must have the same type (got P<int> and P<X>)
+ResolutionErrors.dfy(1111,13): Error: arguments must have the same type (got P<bool> and P<X>)
+ResolutionErrors.dfy(1112,13): Error: arguments must have the same type (got P<int> and P<bool>)
+ResolutionErrors.dfy(1130,31): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+ResolutionErrors.dfy(1132,38): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+ResolutionErrors.dfy(1137,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1230,13): Error: type variable 'PT' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(1231,14): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1231,19): Error: type variable 'QT' in the function call to 'Q' could not be determined
+ResolutionErrors.dfy(1232,4): Error: type '?' to the method 'M' is not determined
+ResolutionErrors.dfy(1233,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1233,13): Error: type '?' to the method 'N' is not determined
+ResolutionErrors.dfy(1234,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1235,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1236,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(1237,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1238,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(1242,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1242,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1243,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1244,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1244,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1251,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(1254,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1270,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1271,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1308,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1318,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1346,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
+ResolutionErrors.dfy(1356,29): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1358,49): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1358,54): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1379,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1379,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1380,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1380,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1381,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1381,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)
+ResolutionErrors.dfy(1382,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1382,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)
+ResolutionErrors.dfy(1387,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1387,13): Error: arguments must have the same type (got int and #type)
+ResolutionErrors.dfy(1388,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1388,13): Error: arguments must have the same type (got int and #module)
+ResolutionErrors.dfy(1389,4): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1390,4): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1399,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1400,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1401,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1404,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(1447,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1469,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1470,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1471,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1474,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1456,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1469,18): 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(1498,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1499,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1500,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1503,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1491,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1498,18): 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(1527,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1420,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1422,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1538,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1556,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(1568,16): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(1575,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1581,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(1598,8): 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(1607,26): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1615,6): Error: the type of the bound variable 't' could not be determined
+ResolutionErrors.dfy(1633,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1635,10): 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(1660,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1662,25): 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)
+ResolutionErrors.dfy(1663,35): 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)
+ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1677,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)
+ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1691,29): 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)
+ResolutionErrors.dfy(1699,17): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1700,19): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1703,23): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1707,36): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1709,34): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor
+ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
+ResolutionErrors.dfy(475,6): Error: when allocating an object of type 'Y', one of its constructor methods must be called
+ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called
+ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called
+ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor
+ResolutionErrors.dfy(853,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
+ResolutionErrors.dfy(857,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1053,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1056,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1059,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1061,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1063,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(12,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
 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>)
@@ -144,42 +197,36 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex
 ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
 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(260,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(265,2): Error: duplicate label
-ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated
-ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)
-ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)
-ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
-ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
-ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)
-ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(386,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(470,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(549,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses
-ResolutionErrors.dfy(918,9): Error: unresolved identifier: s
-ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
-ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int
-ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3
-ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)
-ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)
-ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
-ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-ResolutionErrors.dfy(1134,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(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-184 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(301,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(306,2): Error: duplicate label
+ResolutionErrors.dfy(332,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(333,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(335,9): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(349,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(350,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(351,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(387,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(399,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+ResolutionErrors.dfy(407,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
+ResolutionErrors.dfy(412,6): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(415,6): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(415,6): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(416,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(416,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(421,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(421,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(580,18): Error: unresolved identifier: w
+ResolutionErrors.dfy(686,11): Error: lemmas are not allowed to have modifies clauses
+ResolutionErrors.dfy(935,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(946,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(947,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(953,16): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(954,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(954,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(977,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(978,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
+ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+ResolutionErrors.dfy(1151,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(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+231 resolution/type errors detected in ResolutionErrors.dfy