ResolutionErrors.dfy(502,7): Error: RHS (of type List) not assignable to LHS (of type List) ResolutionErrors.dfy(507,7): Error: RHS (of type List) not assignable to LHS (of type List) 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) ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq) 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 or declare a module import 'opened?') ResolutionErrors.dfy(998,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(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 or declare a module import 'opened?') ResolutionErrors.dfy(1077,6): Error: RHS (of type P) not assignable to LHS (of type P) ResolutionErrors.dfy(1082,6): Error: RHS (of type P) not assignable to LHS (of type P) ResolutionErrors.dfy(1087,6): Error: RHS (of type P) not assignable to LHS (of type P) ResolutionErrors.dfy(1088,6): Error: RHS (of type P) not assignable to LHS (of type P) ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P and P) ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P and P) ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P and P) 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 or declare a module import 'opened?') ResolutionErrors.dfy(1254,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(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(1362,11): Error: name of type (X) is used as a variable ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable ResolutionErrors.dfy(1364,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) ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1365,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) ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type) ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module) ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int) ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int) ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int) ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int) 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 ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts 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(24,11): Error: array selection requires an array2 (got array3) ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array) 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: 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,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 (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, got GenericClass) ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) 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) 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 202 resolution/type errors detected in ResolutionErrors.dfy