Enabled lit tests for test1/ directory

Bizarely Array.bpl does not pass on Windows. This will be fixed soon.

33 files changed, 351 insertions, 151 deletions

diff --git a/Test/test1/Answer b/Test/test1/Answer
index b79a01f8..403b4289 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -1,168 +1,168 @@
-Frame0.bpl(10,11): Error: undeclared identifier: a

-Frame0.bpl(12,11): Error: undeclared identifier: b

+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(16,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

-Frame1.bpl(17,6): Error: command assigns to an immutable variable: a

-Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

-Frame1.bpl(23,4): Error: command assigns to an immutable variable: a

-Frame1.bpl(27,12): Error: command assigns to an immutable variable: hh

-Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

-Frame1.bpl(30,7): Error: command assigns to an immutable variable: hh

-Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

-Frame1.bpl(33,4): Error: command assigns to an immutable variable: hh

-Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

-Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

-Frame1.bpl(84,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x

-Frame1.bpl(89,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)

+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(15,14): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(16,14): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(20,7): Error: wrong number of arguments in map assignment: 2 instead of 1

-Arrays.bpl(21,7): Error: wrong number of arguments in map assignment: 1 instead of 2

-Arrays.bpl(41,13): Error: invalid type for argument 0 in map select: bool (expected: int)

-Arrays.bpl(42,16): Error: invalid argument types (bool and int) to binary operator ==

-Arrays.bpl(43,13): Error: invalid type for argument 0 in map select: int (expected: bool)

-Arrays.bpl(43,15): Error: invalid type for argument 1 in map select: int (expected: ref)

-Arrays.bpl(44,15): Error: invalid type for argument 1 in map select: bool (expected: ref)

-Arrays.bpl(44,23): Error: invalid type for argument 0 in map select: ref (expected: bool)

-Arrays.bpl(45,13): Error: invalid type for argument 0 in map select: ref (expected: bool)

-Arrays.bpl(45,18): Error: invalid type for argument 1 in map select: int (expected: ref)

-Arrays.bpl(45,2): Error: preconditions must be of type bool

-Arrays.bpl(46,13): Error: invalid type for argument 0 in map select: int (expected: bool)

-Arrays.bpl(46,15): Error: invalid type for argument 1 in map select: int (expected: ref)

-Arrays.bpl(50,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-Arrays.bpl(51,6): Error: invalid type for argument 0 in map assignment: int (expected: bool)

-Arrays.bpl(51,8): Error: invalid type for argument 1 in map assignment: int (expected: ref)

-Arrays.bpl(51,5): Error: mismatched types in assignment command (cannot assign ref to int)

-Arrays.bpl(52,7): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-Arrays.bpl(52,5): Error: mismatched types in assignment command (cannot assign int to bool)

-Arrays.bpl(53,12): Error: invalid type for argument 1 in map assignment: bool (expected: ref)

-Arrays.bpl(113,11): Error: invalid type for argument 0 in map select: name (expected: [int,int]bool)

-Arrays.bpl(114,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to [[int,int]bool,[name]name]int)

-Arrays.bpl(115,4): Error: mismatched types in assignment command (cannot assign name to [int,int]bool)

-Arrays.bpl(116,5): Error: mismatched types in assignment command (cannot assign name to bool)

-Arrays.bpl(117,8): Error: invalid type for argument 1 in map assignment: name (expected: [name]name)

-Arrays.bpl(118,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [[int,int]bool,[name]name]int)

-Arrays.bpl(123,10): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(124,14): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(125,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-Arrays.bpl(126,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [int,int][name]int)

-Arrays.bpl(127,4): Error: mismatched types in assignment command (cannot assign [int,int][name]int to [int,int][int]int)

-Arrays.bpl(130,21): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(131,5): Error: wrong number of arguments in map assignment: 2 instead of 1

-Arrays.bpl(132,13): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(133,17): Error: wrong number of arguments in map select: 1 instead of 2

-Arrays.bpl(134,14): Error: wrong number of arguments in map select: 2 instead of 1

-Arrays.bpl(166,12): Error: invalid type for argument 0 in application of Sf: [int,int]bool (expected: any)

-Arrays.bpl(176,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to <a>[int,a]bool)

-Arrays.bpl(177,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [int,int]bool)

-Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to <a>[int,a]bool)

-Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [any,any]bool)

-Arrays.bpl(180,4): Error: mismatched types in assignment command (cannot assign [ref]bool to [any]bool)

-Arrays.bpl(191,18): Error: invalid type for argument 0 in map select: any (expected: int)

-Arrays.bpl(198,11): Error: invalid type for argument 0 in map assignment: any (expected: int)

-Arrays.bpl(214,24): Error: invalid type for argument 0 in call to IntMethod: int (expected: any)

-Arrays.bpl(214,9): Error: invalid type for out-parameter 0 in call to IntMethod: any (expected: int)

-Arrays.bpl(215,4): Error: mismatched types in assignment command (cannot assign int to any)

-Arrays.bpl(216,4): Error: mismatched types in assignment command (cannot assign any to int)

-Arrays.bpl(218,24): Error: invalid type for argument 0 in call to AnyMethod: any (expected: int)

-Arrays.bpl(218,9): Error: invalid type for out-parameter 0 in call to AnyMethod: int (expected: any)

+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(25,34): Error: invalid argument types (double and int) to binary operator +

-WhereTyping.bpl(26,12): Error: where clauses must be of type bool

-WhereTyping.bpl(36,22): Error: invalid argument types (name and int) to binary operator !=

-WhereTyping.bpl(41,30): Error: invalid argument types (name and int) to binary operator ==

+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(30,4): Error: mismatched types in assignment command (cannot assign int to bool)

-Family.bpl(31,8): Error: mismatched types in assignment command (cannot assign bool to int)

-Family.bpl(33,8): Error: mismatched types in assignment command (cannot assign int to y)

-Family.bpl(34,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

-Family.bpl(35,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

-Family.bpl(37,8): Error: mismatched types in assignment command (cannot assign bool to any)

-Family.bpl(38,8): Error: mismatched types in assignment command (cannot assign Field any to any)

-Family.bpl(39,8): Error: mismatched types in assignment command (cannot assign Field y to any)

+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(3,23): Error: ++ operands need to be bitvectors (got int, int)

-AttributeTyping.bpl(5,29): Error: invalid type for argument 0 in application of F0: bool (expected: int)

-AttributeTyping.bpl(7,26): Error: invalid type for argument 0 in application of F0: bool (expected: int)

-AttributeTyping.bpl(9,21): Error: invalid argument types (int and int) to binary operator &&

-AttributeTyping.bpl(11,22): Error: invalid argument type (int) to unary operator !

-AttributeTyping.bpl(13,32): Error: invalid argument types (int and int) to binary operator ==>

+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(3,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

-UpdateExprTyping.bpl(4,11): Error: invalid argument types ([int]bool and [bool]bool) to binary operator ==

-UpdateExprTyping.bpl(7,16): Error: invalid type for argument 0 in map store: bool (expected: int)

-UpdateExprTyping.bpl(8,21): Error: right-hand side in map store with wrong type: int (expected: bool)

-UpdateExprTyping.bpl(9,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

-UpdateExprTyping.bpl(15,18): Error: invalid type for argument 0 in map store: ref (expected: int)

-UpdateExprTyping.bpl(16,20): Error: invalid type for argument 1 in map store: bool (expected: ref)

-UpdateExprTyping.bpl(17,28): Error: right-hand side in map store with wrong type: ref (expected: bool)

-UpdateExprTyping.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to any)

-UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type: ref (expected: any)

-UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)

-UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)

+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(26,6): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: m

-MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)

-MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)

-MapsTypeErrors.bpl(39,3): Error: mismatched types in assignment command (cannot assign bool to int)

-MapsTypeErrors.bpl(67,14): Error: invalid argument types (Field int and Field bool) to binary operator ==

-MapsTypeErrors.bpl(70,27): Error: invalid type for argument 1 in application of StrictEqual: Field bool (expected: a)

-MapsTypeErrors.bpl(75,33): Error: invalid type for argument 1 in application of StrictEqual: Field int (expected: a)

-MapsTypeErrors.bpl(77,31): Error: invalid type for argument 1 in application of IntEqual: Field alpha (expected: Field int)

-MapsTypeErrors.bpl(90,8): Error: extract operand must be a bitvector of at least 32 bits (got bv31)

-MapsTypeErrors.bpl(91,8): Error: extract operand must be a bitvector of at least 32 bits (got int)

-MapsTypeErrors.bpl(95,2): Error: mismatched types in assignment command (cannot assign bv33 to bv32)

-MapsTypeErrors.bpl(104,2): Error: mismatched types in assignment command (cannot assign bv20 to bv32)

-MapsTypeErrors.bpl(110,56): Error: invalid type for argument 1 in application of Same: bv18 (expected: T)

-MapsTypeErrors.bpl(120,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to [int,int]bool)

-MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to HeapType)

+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(6,19): Error: parent of constant has incompatible type (int instead of C)

+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(19,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

+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(6,45): Error: function body with invalid type: bool (expected: int)

-FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)

-FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)

+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(5,7): Error: the first argument to if-then-else should be bool, not int

-IfThenElse0.bpl(6,7): Error: branches of if-then-else have incompatible types bool and int

-IfThenElse0.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to bool)

+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(5,2): Error: mismatched types in assignment command (cannot assign [int]int to [int,int]int)

-Lambda.bpl(6,2): Error: mismatched types in assignment command (cannot assign [int]int to [int]bool)

-Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lambda parameters

-Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)

-Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +

+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(5,8): Error: invalid argument types (int and real) to binary operator >=

-IntReal.bpl(6,8): Error: invalid argument types (int and real) to binary operator <=

-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(10,9): Error: invalid argument types (int and real) to binary operator ==

-IntReal.bpl(11,8): Error: invalid argument types (int and real) to binary operator +

-IntReal.bpl(12,8): 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 div

-IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator mod

-IntReal.bpl(17,12): Error: invalid argument types (real and int) to binary operator ==

-IntReal.bpl(23,8): Error: invalid argument types (int and real) to binary operator **

-IntReal.bpl(27,14): Error: invalid argument types (real and int) to binary operator ==

-IntReal.bpl(29,13): Error: invalid argument types (int and real) to binary operator ==

-IntReal.bpl(32,6): Error: argument type int does not match expected type real

-IntReal.bpl(33,6): Error: argument type real does not match expected type int

-IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div

-IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod

+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(3,22): Error: assumption variable may not be declared with a where clause

-AssumptionVariables0.bpl(19,7): Error: RHS of assignment to assumption variable a0 must match expression "a0 && <boolean expression>"

-AssumptionVariables0.bpl(28,7): Error: RHS of assignment to assumption variable a0 must match expression "a0 && <boolean expression>"

-AssumptionVariables0.bpl(37,7): Error: assumption variable may not be assigned to more than once

-AssumptionVariables0.bpl(54,7): Error: assumption variable may not be assigned to more than once

+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

diff --git a/Test/test1/Arrays.bpl b/Test/test1/Arrays.bpl
index 85ee783b..9f1d47ba 100644
--- a/Test/test1/Arrays.bpl
+++ b/Test/test1/Arrays.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 var one: [int]int;

 var two: [int, int]int;

 

diff --git a/Test/test1/Arrays.bpl.expect b/Test/test1/Arrays.bpl.expect
new file mode 100644
index 00000000..a9829c61
--- /dev/null
+++ b/Test/test1/Arrays.bpl.expect
@@ -0,0 +1,53 @@
+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
diff --git a/Test/test1/AssumptionVariables0.bpl b/Test/test1/AssumptionVariables0.bpl
index 4185ffd3..5cc202b0 100644
--- a/Test/test1/AssumptionVariables0.bpl
+++ b/Test/test1/AssumptionVariables0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 procedure Test0()

 {

     var {:assumption} a0: bool where a0;  // error

diff --git a/Test/test1/AssumptionVariables0.bpl.expect b/Test/test1/AssumptionVariables0.bpl.expect
new file mode 100644
index 00000000..b1291a38
--- /dev/null
+++ b/Test/test1/AssumptionVariables0.bpl.expect
@@ -0,0 +1,6 @@
+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
diff --git a/Test/test1/AttributeTyping.bpl b/Test/test1/AttributeTyping.bpl
index 204ac2ac..d500beca 100644
--- a/Test/test1/AttributeTyping.bpl
+++ b/Test/test1/AttributeTyping.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 

 

 const {:Incorrect pux0 ++ F0(pux1)} pux0: int;

diff --git a/Test/test1/AttributeTyping.bpl.expect b/Test/test1/AttributeTyping.bpl.expect
new file mode 100644
index 00000000..f5348ced
--- /dev/null
+++ b/Test/test1/AttributeTyping.bpl.expect
@@ -0,0 +1,7 @@
+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
diff --git a/Test/test1/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl
index 31e4b43f..2df52288 100644
--- a/Test/test1/EmptyCallArgs.bpl
+++ b/Test/test1/EmptyCallArgs.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 type C;

 

 procedure P(x:int, y:bool) returns (z:C);

diff --git a/Test/test1/EmptyCallArgs.bpl.expect b/Test/test1/EmptyCallArgs.bpl.expect
new file mode 100644
index 00000000..82ed9ad3
--- /dev/null
+++ b/Test/test1/EmptyCallArgs.bpl.expect
@@ -0,0 +1,2 @@
+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
diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl
index 1c650d3d..00657658 100644
--- a/Test/test1/Family.bpl
+++ b/Test/test1/Family.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 type T;

 

 var Heap: <x>[ref,Field x]x;

diff --git a/Test/test1/Family.bpl.expect b/Test/test1/Family.bpl.expect
new file mode 100644
index 00000000..143e940c
--- /dev/null
+++ b/Test/test1/Family.bpl.expect
@@ -0,0 +1,9 @@
+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
diff --git a/Test/test1/Frame0.bpl b/Test/test1/Frame0.bpl
index 02a5af46..72443d46 100644
--- a/Test/test1/Frame0.bpl
+++ b/Test/test1/Frame0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 var g0: int;

 var g1: int;

 

diff --git a/Test/test1/Frame0.bpl.expect b/Test/test1/Frame0.bpl.expect
new file mode 100644
index 00000000..5c4c229d
--- /dev/null
+++ b/Test/test1/Frame0.bpl.expect
@@ -0,0 +1,3 @@
+Frame0.bpl(12,11): Error: undeclared identifier: a
+Frame0.bpl(14,11): Error: undeclared identifier: b
+2 name resolution errors detected in Frame0.bpl
diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl
index 469f43ba..23f94488 100644
--- a/Test/test1/Frame1.bpl
+++ b/Test/test1/Frame1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 var g0: int;

 var g1: int;

 

diff --git a/Test/test1/Frame1.bpl.expect b/Test/test1/Frame1.bpl.expect
new file mode 100644
index 00000000..4e12181d
--- /dev/null
+++ b/Test/test1/Frame1.bpl.expect
@@ -0,0 +1,17 @@
+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
diff --git a/Test/test1/FunBody.bpl b/Test/test1/FunBody.bpl
index 867942ff..565b00e5 100644
--- a/Test/test1/FunBody.bpl
+++ b/Test/test1/FunBody.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 

 function g0<beta>(x:beta) returns (beta);

 function g1<beta>() returns (beta);

diff --git a/Test/test1/FunBody.bpl.expect b/Test/test1/FunBody.bpl.expect
new file mode 100644
index 00000000..6ed90fd5
--- /dev/null
+++ b/Test/test1/FunBody.bpl.expect
@@ -0,0 +1,4 @@
+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
diff --git a/Test/test1/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl
index c26461b1..18c58cb2 100644
--- a/Test/test1/IfThenElse0.bpl
+++ b/Test/test1/IfThenElse0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 procedure foo()
 {
   var b:bool, i:int;
diff --git a/Test/test1/IfThenElse0.bpl.expect b/Test/test1/IfThenElse0.bpl.expect
new file mode 100644
index 00000000..87f78751
--- /dev/null
+++ b/Test/test1/IfThenElse0.bpl.expect
@@ -0,0 +1,4 @@
+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
diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl
index 976fc864..c816d05c 100644
--- a/Test/test1/IntReal.bpl
+++ b/Test/test1/IntReal.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 const i: int;

 const r: real;

 

diff --git a/Test/test1/IntReal.bpl.expect b/Test/test1/IntReal.bpl.expect
new file mode 100644
index 00000000..021a8389
--- /dev/null
+++ b/Test/test1/IntReal.bpl.expect
@@ -0,0 +1,19 @@
+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
diff --git a/Test/test1/Lambda.bpl b/Test/test1/Lambda.bpl
index d0ccd3a1..70a61ea8 100644
--- a/Test/test1/Lambda.bpl
+++ b/Test/test1/Lambda.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 procedure foo()
 {
   var a: [int,int]int;
diff --git a/Test/test1/Lambda.bpl.expect b/Test/test1/Lambda.bpl.expect
new file mode 100644
index 00000000..a917f0fa
--- /dev/null
+++ b/Test/test1/Lambda.bpl.expect
@@ -0,0 +1,6 @@
+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
diff --git a/Test/test1/LogicalExprs.bpl b/Test/test1/LogicalExprs.bpl
index 028d18f4..e63e3dce 100644
--- a/Test/test1/LogicalExprs.bpl
+++ b/Test/test1/LogicalExprs.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 const P: bool;

 const Q: bool;

 

diff --git a/Test/test1/LogicalExprs.bpl.expect b/Test/test1/LogicalExprs.bpl.expect
new file mode 100644
index 00000000..cc5cde4d
--- /dev/null
+++ b/Test/test1/LogicalExprs.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test1/MapsTypeErrors.bpl b/Test/test1/MapsTypeErrors.bpl
index 0e68440d..135cb7e7 100644
--- a/Test/test1/MapsTypeErrors.bpl
+++ b/Test/test1/MapsTypeErrors.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 var m: []int;

 var p: <a>[]a;

 

diff --git a/Test/test1/MapsTypeErrors.bpl.expect b/Test/test1/MapsTypeErrors.bpl.expect
new file mode 100644
index 00000000..9195f868
--- /dev/null
+++ b/Test/test1/MapsTypeErrors.bpl.expect
@@ -0,0 +1,16 @@
+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
diff --git a/Test/test1/Orderings.bpl b/Test/test1/Orderings.bpl
index be0502fa..17d4aea9 100644
--- a/Test/test1/Orderings.bpl
+++ b/Test/test1/Orderings.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 

 type C;

 

diff --git a/Test/test1/Orderings.bpl.expect b/Test/test1/Orderings.bpl.expect
new file mode 100644
index 00000000..8844489d
--- /dev/null
+++ b/Test/test1/Orderings.bpl.expect
@@ -0,0 +1,2 @@
+Orderings.bpl(8,19): Error: parent of constant has incompatible type (int instead of C)
+1 type checking errors detected in Orderings.bpl
diff --git a/Test/test1/UpdateExprTyping.bpl b/Test/test1/UpdateExprTyping.bpl
index e495cb51..cc1d5e40 100644
--- a/Test/test1/UpdateExprTyping.bpl
+++ b/Test/test1/UpdateExprTyping.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 procedure P(a: [int]bool, b: [int]ref, c: [bool]bool)

 {

   assert a == b;  // type error

diff --git a/Test/test1/UpdateExprTyping.bpl.expect b/Test/test1/UpdateExprTyping.bpl.expect
new file mode 100644
index 00000000..0cee7e03
--- /dev/null
+++ b/Test/test1/UpdateExprTyping.bpl.expect
@@ -0,0 +1,13 @@
+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
diff --git a/Test/test1/WhereTyping.bpl b/Test/test1/WhereTyping.bpl
index dba628ee..c48590bf 100644
--- a/Test/test1/WhereTyping.bpl
+++ b/Test/test1/WhereTyping.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t

+// RUN: %diff %s.expect %t

 var g: int where g == 12;

 

 procedure P(x: int where x > 0) returns (y: int where y < 0);

diff --git a/Test/test1/WhereTyping.bpl.expect b/Test/test1/WhereTyping.bpl.expect
new file mode 100644
index 00000000..4daa572a
--- /dev/null
+++ b/Test/test1/WhereTyping.bpl.expect
@@ -0,0 +1,5 @@
+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