TypeDecls0.bpl(20,5): Error: more than one declaration of type name: C TypeDecls0.bpl(13,12): Error: more than one declaration of type variable: a TypeDecls0.bpl(14,18): Error: more than one declaration of type variable: a TypeDecls0.bpl(18,17): Error: type variable must occur in map arguments: b TypeDecls0.bpl(22,9): Error: type constructor received wrong number of arguments: C TypeDecls0.bpl(24,9): Error: undeclared type: A0 TypeDecls0.bpl(25,9): Error: undeclared type: F TypeDecls0.bpl(28,9): Error: type constructor received wrong number of arguments: E TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E TypeDecls0.bpl(38,11): Error: type constructor received wrong number of arguments: E TypeDecls0.bpl(38,13): Error: type constructor received wrong number of arguments: E 12 name resolution errors detected in TypeDecls0.bpl TypeDecls1.bpl(7,13): Error: invalid type for argument 0 in map select: int (expected: [b]a) TypeDecls1.bpl(13,25): Error: right-hand side in map store with wrong type: int (expected: bool) TypeDecls1.bpl(19,36): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: [[b]a]bool (expected: [b]a) 4 type checking errors detected in TypeDecls1.bpl Prog0.bpl(17,10): Error: type variable must occur in map arguments: a Prog0.bpl(29,27): Error: more than one declaration of type variable: beta Prog0.bpl(32,22): Error: undeclared type: alpha Prog0.bpl(33,35): Error: undeclared type: alpha 4 name resolution errors detected in Prog0.bpl Prog1.bpl(18,11): Error: invalid type for argument 0 in map select: int (expected: ref) Prog1.bpl(19,14): Error: invalid type for argument 1 in map select: int (expected: Field a) Prog1.bpl(20,17): Error: invalid argument types (bool and int) to binary operator >= 3 type checking errors detected in Prog1.bpl Prog2.bpl(6,14): Error: trigger does not mention alpha, which does not occur in variables types either 1 type checking errors detected in Prog2.bpl PolyFuns0.bpl(23,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a) PolyFuns0.bpl(40,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a) PolyFuns0.bpl(41,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a) PolyFuns0.bpl(53,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == 4 type checking errors detected in PolyFuns0.bpl PolyFuns1.bpl(10,9): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) PolyFuns1.bpl(17,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == PolyFuns1.bpl(18,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu:
[Field dd]dd (expected: [Field c]a) PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: [Field cc]T (expected: [Field d]d) PolyFuns1.bpl(30,12): Error: invalid argument types ([Field cc]T and
[Field dd]dd) to binary operator == PolyFuns1.bpl(31,12): Error: invalid argument types (
[Field dd]dd and [Field cc]T) to binary operator == PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: [Field T]ee (expected: [Field d]d) PolyFuns1.bpl(41,11): Error: invalid argument types ([a,a]int and [b,int]int) to binary operator == PolyFuns1.bpl(42,11): Error: invalid argument types ([b,int]int and [int,c]int) to binary operator == PolyFuns1.bpl(43,11): Error: invalid argument types ([a,a]int and [int,c]int) to binary operator == PolyFuns1.bpl(50,11): Error: invalid argument types ([a,a,b]int and [a,b,b]int) to binary operator == PolyFuns1.bpl(57,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator == 16 type checking errors detected in PolyFuns1.bpl PolyProcs0.bpl(11,16): Error: invalid type for argument 0 in map select: Field b (expected: ref) PolyProcs0.bpl(11,19): Error: invalid type for argument 1 in map select: ref (expected: Field a) PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref) PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int) PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref) 7 type checking errors detected in PolyProcs0.bpl TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) TypeSynonyms0.bpl(22,10): Error: type constructor received wrong number of arguments: Field TypeSynonyms0.bpl(23,10): Error: type synonym received wrong number of arguments: Set TypeSynonyms0.bpl(26,10): Error: type variable must occur in map arguments: a 6 name resolution errors detected in TypeSynonyms0.bpl TypeSynonyms1.bpl(46,8): Error: invalid type for argument 0 in application of h: [b,b,[b2,b,int]int]int (expected: nested2) 1 type checking errors detected in TypeSynonyms1.bpl Boogie program verifier finished with 1 verified, 0 errors type Set a = [a]bool; type Field _; type Heap = [ref,Field a]a; type notAllParams a b = Field b; type Cyclic0 = Cyclic1; type Cyclic1 = Cyclic0; type AlsoCyclic a = [AlsoCyclic b]int; type C _ _; type C2 b a = C a b; function f(C int bool) : int; const x: C2 bool int; const y: Field int bool; const z: Set int bool; const d: [notAllParams a b]int; type ref; (10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) (12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) (14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) (24,8): Error: type constructor received wrong number of arguments: Field (26,8): Error: type synonym received wrong number of arguments: Set (28,8): Error: type variable must occur in map arguments: a 6 name resolution errors detected in TypeSynonyms0.bpl type Set a = [a]bool; function union(x: Set a, y: Set a) : Set a; axiom (forall x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]); const intSet0: Set int; axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); const intSet1: Set int; axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3)); procedure P(); implementation P() { assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3)); } type Set a = [a]bool; function union(x: Set a, y: Set a) : Set a; axiom (forall x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]); const intSet0: Set int; axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3); const intSet1: Set int; axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3); procedure P(); implementation P() { assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3); } Boogie program verifier finished with 0 verified, 0 errors PolyPolyPoly.bpl(12,26): Error: invalid argument types ([]? and []C a) to binary operator == PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and []C a) to binary operator == PolyPolyPoly.bpl(21,57): Error: invalid type for argument 1 in map select: b (expected: a) 3 type checking errors detected in PolyPolyPoly.bpl PolyPolyPoly2.bpl(5,8): Warning: type parameter a is ambiguous, instantiating to int PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to [arg0]res PolyPolyPoly2.bpl(11,8): Warning: type parameter a is ambiguous, instantiating to bv0 PolyPolyPoly2.bpl(11,15): Warning: type parameter a is ambiguous, instantiating to bv0 PolyPolyPoly2.bpl(11,27): Warning: type parameter a is ambiguous, instantiating to bv17 PolyPolyPoly2.bpl(12,8): Warning: type parameter a is ambiguous, instantiating to bv17 PolyPolyPoly2.bpl(12,15): Warning: type parameter a is ambiguous, instantiating to bv0 PolyPolyPoly2.bpl(22,7): Warning: type parameter a is ambiguous, instantiating to int PolyPolyPoly2.bpl(31,3): Warning: type parameter a is ambiguous, instantiating to int PolyPolyPoly2.bpl(32,3): Warning: type parameter a is ambiguous, instantiating to int Boogie program verifier finished with 0 verified, 0 errors ProcParamReordering.bpl(13,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation) ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in procedure implementation: P 2 type checking errors detected in ProcParamReordering.bpl ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int) ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int) ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z 3 type checking errors detected in ParallelAssignment.bpl ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment 2 name resolution errors detected in ParallelAssignment2.bpl Coercions.bpl(11,8): Error: int cannot be coerced to E [a]int Coercions.bpl(13,8): Error: C cannot be coerced to D Coercions.bpl(15,9): Error: int cannot be coerced to D Coercions.bpl(16,9): Error: int cannot be coerced to E int 4 type checking errors detected in Coercions.bpl Boogie program verifier finished with 0 verified, 0 errors