Frame0.bpl(12,11): Error: undeclared identifier: a
Frame0.bpl(14,11): Error: undeclared identifier: b
2 name resolution errors detected in Frame0.bpl
Frame1.bpl(18,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1
Frame1.bpl(19,6): Error: command assigns to an immutable variable: a
Frame1.bpl(24,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1
Frame1.bpl(25,4): Error: command assigns to an immutable variable: a
Frame1.bpl(29,12): Error: command assigns to an immutable variable: hh
Frame1.bpl(30,12): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0
Frame1.bpl(32,7): Error: command assigns to an immutable variable: hh
Frame1.bpl(33,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0
Frame1.bpl(35,4): Error: command assigns to an immutable variable: hh
Frame1.bpl(36,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0
Frame1.bpl(57,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0
Frame1.bpl(70,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0
Frame1.bpl(70,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1
Frame1.bpl(70,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0
Frame1.bpl(86,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x
Frame1.bpl(91,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)
16 type checking errors detected in Frame1.bpl

Boogie program verifier finished with 0 verified, 0 errors
Arrays.bpl(17,14): Error: wrong number of arguments in map select: 2 instead of 1
Arrays.bpl(18,14): Error: wrong number of arguments in map select: 1 instead of 2
Arrays.bpl(22,7): Error: wrong number of arguments in map assignment: 2 instead of 1
Arrays.bpl(23,7): Error: wrong number of arguments in map assignment: 1 instead of 2
Arrays.bpl(43,13): Error: invalid type for argument 0 in map select: bool (expected: int)
Arrays.bpl(44,16): Error: invalid argument types (bool and int) to binary operator ==
Arrays.bpl(45,13): Error: invalid type for argument 0 in map select: int (expected: bool)
Arrays.bpl(45,15): Error: invalid type for argument 1 in map select: int (expected: ref)
Arrays.bpl(46,15): Error: invalid type for argument 1 in map select: bool (expected: ref)
Arrays.bpl(46,23): Error: invalid type for argument 0 in map select: ref (expected: bool)
Arrays.bpl(47,13): Error: invalid type for argument 0 in map select: ref (expected: bool)
Arrays.bpl(47,18): Error: invalid type for argument 1 in map select: int (expected: ref)
Arrays.bpl(47,2): Error: preconditions must be of type bool
Arrays.bpl(48,13): Error: invalid type for argument 0 in map select: int (expected: bool)
Arrays.bpl(48,15): Error: invalid type for argument 1 in map select: int (expected: ref)
Arrays.bpl(52,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)
Arrays.bpl(53,6): Error: invalid type for argument 0 in map assignment: int (expected: bool)
Arrays.bpl(53,8): Error: invalid type for argument 1 in map assignment: int (expected: ref)
Arrays.bpl(53,5): Error: mismatched types in assignment command (cannot assign ref to int)
Arrays.bpl(54,7): Error: invalid type for argument 0 in map assignment: bool (expected: int)
Arrays.bpl(54,5): Error: mismatched types in assignment command (cannot assign int to bool)
Arrays.bpl(55,12): Error: invalid type for argument 1 in map assignment: bool (expected: ref)
Arrays.bpl(115,11): Error: invalid type for argument 0 in map select: name (expected: [int,int]bool)
Arrays.bpl(116,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to [[int,int]bool,[name]name]int)
Arrays.bpl(117,4): Error: mismatched types in assignment command (cannot assign name to [int,int]bool)
Arrays.bpl(118,5): Error: mismatched types in assignment command (cannot assign name to bool)
Arrays.bpl(119,8): Error: invalid type for argument 1 in map assignment: name (expected: [name]name)
Arrays.bpl(120,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [[int,int]bool,[name]name]int)
Arrays.bpl(125,10): Error: wrong number of arguments in map select: 1 instead of 2
Arrays.bpl(126,14): Error: wrong number of arguments in map select: 1 instead of 2
Arrays.bpl(127,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)
Arrays.bpl(128,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [int,int][name]int)
Arrays.bpl(129,4): Error: mismatched types in assignment command (cannot assign [int,int][name]int to [int,int][int]int)
Arrays.bpl(132,21): Error: wrong number of arguments in map select: 2 instead of 1
Arrays.bpl(133,5): Error: wrong number of arguments in map assignment: 2 instead of 1
Arrays.bpl(134,13): Error: wrong number of arguments in map select: 2 instead of 1
Arrays.bpl(135,17): Error: wrong number of arguments in map select: 1 instead of 2
Arrays.bpl(136,14): Error: wrong number of arguments in map select: 2 instead of 1
Arrays.bpl(168,12): Error: invalid type for argument 0 in application of Sf: [int,int]bool (expected: any)
Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to <a>[int,a]bool)
Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [int,int]bool)
Arrays.bpl(180,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to <a>[int,a]bool)
Arrays.bpl(181,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [any,any]bool)
Arrays.bpl(182,4): Error: mismatched types in assignment command (cannot assign [ref]bool to [any]bool)
Arrays.bpl(193,18): Error: invalid type for argument 0 in map select: any (expected: int)
Arrays.bpl(200,11): Error: invalid type for argument 0 in map assignment: any (expected: int)
Arrays.bpl(216,24): Error: invalid type for argument 0 in call to IntMethod: int (expected: any)
Arrays.bpl(216,9): Error: invalid type for out-parameter 0 in call to IntMethod: any (expected: int)
Arrays.bpl(217,4): Error: mismatched types in assignment command (cannot assign int to any)
Arrays.bpl(218,4): Error: mismatched types in assignment command (cannot assign any to int)
Arrays.bpl(220,24): Error: invalid type for argument 0 in call to AnyMethod: any (expected: int)
Arrays.bpl(220,9): Error: invalid type for out-parameter 0 in call to AnyMethod: int (expected: any)
52 type checking errors detected in Arrays.bpl
WhereTyping.bpl(27,34): Error: invalid argument types (double and int) to binary operator +
WhereTyping.bpl(28,12): Error: where clauses must be of type bool
WhereTyping.bpl(38,22): Error: invalid argument types (name and int) to binary operator !=
WhereTyping.bpl(43,30): Error: invalid argument types (name and int) to binary operator ==
4 type checking errors detected in WhereTyping.bpl
Family.bpl(32,4): Error: mismatched types in assignment command (cannot assign int to bool)
Family.bpl(33,8): Error: mismatched types in assignment command (cannot assign bool to int)
Family.bpl(35,8): Error: mismatched types in assignment command (cannot assign int to y)
Family.bpl(36,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)
Family.bpl(37,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)
Family.bpl(39,8): Error: mismatched types in assignment command (cannot assign bool to any)
Family.bpl(40,8): Error: mismatched types in assignment command (cannot assign Field any to any)
Family.bpl(41,8): Error: mismatched types in assignment command (cannot assign Field y to any)
8 type checking errors detected in Family.bpl
AttributeTyping.bpl(5,23): Error: ++ operands need to be bitvectors (got int, int)
AttributeTyping.bpl(7,29): Error: invalid type for argument 0 in application of F0: bool (expected: int)
AttributeTyping.bpl(9,26): Error: invalid type for argument 0 in application of F0: bool (expected: int)
AttributeTyping.bpl(11,21): Error: invalid argument types (int and int) to binary operator &&
AttributeTyping.bpl(13,22): Error: invalid argument type (int) to unary operator !
AttributeTyping.bpl(15,32): Error: invalid argument types (int and int) to binary operator ==>
6 type checking errors detected in AttributeTyping.bpl
UpdateExprTyping.bpl(5,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==
UpdateExprTyping.bpl(6,11): Error: invalid argument types ([int]bool and [bool]bool) to binary operator ==
UpdateExprTyping.bpl(9,16): Error: invalid type for argument 0 in map store: bool (expected: int)
UpdateExprTyping.bpl(10,21): Error: right-hand side in map store with wrong type: int (expected: bool)
UpdateExprTyping.bpl(11,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==
UpdateExprTyping.bpl(17,18): Error: invalid type for argument 0 in map store: ref (expected: int)
UpdateExprTyping.bpl(18,20): Error: invalid type for argument 1 in map store: bool (expected: ref)
UpdateExprTyping.bpl(19,28): Error: right-hand side in map store with wrong type: ref (expected: bool)
UpdateExprTyping.bpl(34,2): Error: mismatched types in assignment command (cannot assign int to any)
UpdateExprTyping.bpl(38,28): Error: right-hand side in map store with wrong type: ref (expected: any)
UpdateExprTyping.bpl(40,27): Error: right-hand side in map store with wrong type: ref (expected: int)
UpdateExprTyping.bpl(41,27): Error: right-hand side in map store with wrong type: int (expected: ref)
12 type checking errors detected in UpdateExprTyping.bpl
MapsTypeErrors.bpl(28,6): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: m
MapsTypeErrors.bpl(34,2): Error: mismatched types in assignment command (cannot assign int to []int)
MapsTypeErrors.bpl(35,3): Error: mismatched types in assignment command (cannot assign []int to int)
MapsTypeErrors.bpl(41,3): Error: mismatched types in assignment command (cannot assign bool to int)
MapsTypeErrors.bpl(69,14): Error: invalid argument types (Field int and Field bool) to binary operator ==
MapsTypeErrors.bpl(72,27): Error: invalid type for argument 1 in application of StrictEqual: Field bool (expected: a)
MapsTypeErrors.bpl(77,33): Error: invalid type for argument 1 in application of StrictEqual: Field int (expected: a)
MapsTypeErrors.bpl(79,31): Error: invalid type for argument 1 in application of IntEqual: Field alpha (expected: Field int)
MapsTypeErrors.bpl(92,8): Error: extract operand must be a bitvector of at least 32 bits (got bv31)
MapsTypeErrors.bpl(93,8): Error: extract operand must be a bitvector of at least 32 bits (got int)
MapsTypeErrors.bpl(97,2): Error: mismatched types in assignment command (cannot assign bv33 to bv32)
MapsTypeErrors.bpl(106,2): Error: mismatched types in assignment command (cannot assign bv20 to bv32)
MapsTypeErrors.bpl(112,56): Error: invalid type for argument 1 in application of Same: bv18 (expected: T)
MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to [int,int]bool)
MapsTypeErrors.bpl(124,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to HeapType)
15 type checking errors detected in MapsTypeErrors.bpl
Orderings.bpl(8,19): Error: parent of constant has incompatible type (int instead of C)
1 type checking errors detected in Orderings.bpl
EmptyCallArgs.bpl(21,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
1 type checking errors detected in EmptyCallArgs.bpl
FunBody.bpl(8,45): Error: function body with invalid type: bool (expected: int)
FunBody.bpl(10,61): Error: function body with invalid type: int (expected: alpha)
FunBody.bpl(12,58): Error: function body with invalid type: int (expected: alpha)
3 type checking errors detected in FunBody.bpl
IfThenElse0.bpl(7,7): Error: the first argument to if-then-else should be bool, not int
IfThenElse0.bpl(8,7): Error: branches of if-then-else have incompatible types bool and int
IfThenElse0.bpl(9,2): Error: mismatched types in assignment command (cannot assign int to bool)
3 type checking errors detected in IfThenElse0.bpl
Lambda.bpl(7,2): Error: mismatched types in assignment command (cannot assign [int]int to [int,int]int)
Lambda.bpl(8,2): Error: mismatched types in assignment command (cannot assign [int]int to [int]bool)
Lambda.bpl(14,8): Error: the type variable T does not occur in types of the lambda parameters
Lambda.bpl(14,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)
Lambda.bpl(20,27): Error: invalid argument types (bool and int) to binary operator +
5 type checking errors detected in Lambda.bpl
IntReal.bpl(7,8): Error: invalid argument types (int and real) to binary operator >=
IntReal.bpl(8,8): Error: invalid argument types (int and real) to binary operator <=
IntReal.bpl(9,8): Error: invalid argument types (int and real) to binary operator <
IntReal.bpl(10,8): Error: invalid argument types (int and real) to binary operator >
IntReal.bpl(12,9): Error: invalid argument types (int and real) to binary operator ==
IntReal.bpl(13,8): Error: invalid argument types (int and real) to binary operator +
IntReal.bpl(14,8): Error: invalid argument types (int and real) to binary operator -
IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator *
IntReal.bpl(16,8): Error: invalid argument types (int and real) to binary operator div
IntReal.bpl(17,8): Error: invalid argument types (int and real) to binary operator mod
IntReal.bpl(19,12): Error: invalid argument types (real and int) to binary operator ==
IntReal.bpl(25,8): Error: invalid argument types (int and real) to binary operator **
IntReal.bpl(29,14): Error: invalid argument types (real and int) to binary operator ==
IntReal.bpl(31,13): Error: invalid argument types (int and real) to binary operator ==
IntReal.bpl(34,6): Error: argument type int does not match expected type real
IntReal.bpl(35,6): Error: argument type real does not match expected type int
IntReal.bpl(47,8): Error: invalid argument types (real and int) to binary operator div
IntReal.bpl(48,8): Error: invalid argument types (real and int) to binary operator mod
18 type checking errors detected in IntReal.bpl
AssumptionVariables0.bpl(5,22): Error: assumption variable may not be declared with a where clause
AssumptionVariables0.bpl(21,7): Error: RHS of assignment to assumption variable a0 must match expression "a0 && <boolean expression>"
AssumptionVariables0.bpl(30,7): Error: RHS of assignment to assumption variable a0 must match expression "a0 && <boolean expression>"
AssumptionVariables0.bpl(39,7): Error: assumption variable may not be assigned to more than once
AssumptionVariables0.bpl(56,7): Error: assumption variable may not be assigned to more than once
5 name resolution errors detected in AssumptionVariables0.bpl
AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool'
1 type checking errors detected in AssumptionVariables1.bpl