summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-07 16:24:51 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-07 16:24:51 +0100
commit356ebe6de99459cfb89920b18124aae016206ef0 (patch)
tree1c1dccbf8f0ecf46e01d73c6fb42d34ef3d06a97
parentf6a1c1c597027ad99dbfaea1032dffecff26829e (diff)
Enabled VC Generation lit tests.
-rw-r--r--Test/test2/Answer622
-rw-r--r--Test/test2/Arrays.bpl4
-rw-r--r--Test/test2/Arrays.bpl.expect10
-rw-r--r--Test/test2/AssumeEnsures.bpl2
-rw-r--r--Test/test2/AssumeEnsures.bpl.expect11
-rw-r--r--Test/test2/AssumptionVariables0.bpl2
-rw-r--r--Test/test2/AssumptionVariables0.bpl.expect11
-rw-r--r--Test/test2/Axioms.bpl2
-rw-r--r--Test/test2/Axioms.bpl.expect5
-rw-r--r--Test/test2/B.bpl2
-rw-r--r--Test/test2/B.bpl.expect2
-rw-r--r--Test/test2/Call.bpl2
-rw-r--r--Test/test2/Call.bpl.expect12
-rw-r--r--Test/test2/ContractEvaluationOrder.bpl2
-rw-r--r--Test/test2/ContractEvaluationOrder.bpl.expect13
-rw-r--r--Test/test2/CutBackEdge.bpl2
-rw-r--r--Test/test2/CutBackEdge.bpl.expect13
-rw-r--r--Test/test2/Ensures.bpl2
-rw-r--r--Test/test2/Ensures.bpl.expect22
-rw-r--r--Test/test2/False.bpl2
-rw-r--r--Test/test2/False.bpl.expect2
-rw-r--r--Test/test2/FormulaTerm.bpl2
-rw-r--r--Test/test2/FormulaTerm.bpl.expect6
-rw-r--r--Test/test2/FormulaTerm2.bpl2
-rw-r--r--Test/test2/FormulaTerm2.bpl.expect8
-rw-r--r--Test/test2/FreeCall.bpl2
-rw-r--r--Test/test2/FreeCall.bpl.expect18
-rw-r--r--Test/test2/IfThenElse1.bpl2
-rw-r--r--Test/test2/IfThenElse1.bpl.expect8
-rw-r--r--Test/test2/Implies.bpl2
-rw-r--r--Test/test2/Implies.bpl.expect26
-rw-r--r--Test/test2/Lambda.bpl4
-rw-r--r--Test/test2/Lambda.bpl.expect8
-rw-r--r--Test/test2/LambdaOldExpressions.bpl2
-rw-r--r--Test/test2/LambdaOldExpressions.bpl.expect6
-rw-r--r--Test/test2/LambdaPoly.bpl2
-rw-r--r--Test/test2/LambdaPoly.bpl.expect14
-rw-r--r--Test/test2/LoopInvAssume.bpl2
-rw-r--r--Test/test2/LoopInvAssume.bpl.expect6
-rw-r--r--Test/test2/NeverPattern.bpl2
-rw-r--r--Test/test2/NeverPattern.bpl.expect11
-rw-r--r--Test/test2/NullaryMaps.bpl2
-rw-r--r--Test/test2/NullaryMaps.bpl.expect11
-rw-r--r--Test/test2/Old.bpl2
-rw-r--r--Test/test2/Old.bpl.expect6
-rw-r--r--Test/test2/OldIllegal.bpl2
-rw-r--r--Test/test2/OldIllegal.bpl.expect3
-rw-r--r--Test/test2/Passification.bpl2
-rw-r--r--Test/test2/Passification.bpl.expect20
-rw-r--r--Test/test2/Quantifiers.bpl2
-rw-r--r--Test/test2/Quantifiers.bpl.expect20
-rw-r--r--Test/test2/SelectiveChecking.bpl2
-rw-r--r--Test/test2/SelectiveChecking.bpl.expect16
-rw-r--r--Test/test2/Structured.bpl2
-rw-r--r--Test/test2/Structured.bpl.expect20
-rw-r--r--Test/test2/Timeouts0.bpl2
-rw-r--r--Test/test2/Timeouts0.bpl.expect47
-rw-r--r--Test/test2/TypeEncodingM.bpl2
-rw-r--r--Test/test2/TypeEncodingM.bpl.expect5
-rw-r--r--Test/test2/UpdateExpr.bpl2
-rw-r--r--Test/test2/UpdateExpr.bpl.expect17
-rw-r--r--Test/test2/Where.bpl2
-rw-r--r--Test/test2/Where.bpl.expect37
-rw-r--r--Test/test2/sk_hack.bpl2
-rw-r--r--Test/test2/sk_hack.bpl.expect2
-rw-r--r--Test/test2/strings-no-where.bpl2
-rw-r--r--Test/test2/strings-no-where.bpl.expect19
-rw-r--r--Test/test2/strings-where.bpl2
-rw-r--r--Test/test2/strings-where.bpl.expect19
69 files changed, 837 insertions, 311 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer
index 898655b1..5d446e64 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -1,41 +1,41 @@
-------------------- FormulaTerm.bpl --------------------
-FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold on this return path.
-FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold.
+FormulaTerm.bpl(12,3): Error BP5003: A postcondition might not hold on this return path.
+FormulaTerm.bpl(6,3): Related location: This is the postcondition that might not hold.
Execution trace:
- FormulaTerm.bpl(8,1): start
+ FormulaTerm.bpl(10,1): start
Boogie program verifier finished with 11 verified, 1 error
-------------------- FormulaTerm2.bpl --------------------
-FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold.
+FormulaTerm2.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- FormulaTerm2.bpl(36,3): start
-FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold.
+ FormulaTerm2.bpl(38,3): start
+FormulaTerm2.bpl(49,5): Error BP5001: This assertion might not hold.
Execution trace:
- FormulaTerm2.bpl(45,3): start
+ FormulaTerm2.bpl(47,3): start
Boogie program verifier finished with 2 verified, 2 errors
-------------------- Passification.bpl --------------------
-Passification.bpl(44,3): Error BP5003: A postcondition might not hold on this return path.
-Passification.bpl(36,3): Related location: This is the postcondition that might not hold.
+Passification.bpl(46,3): Error BP5003: A postcondition might not hold on this return path.
+Passification.bpl(38,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Passification.bpl(39,1): A
-Passification.bpl(116,3): Error BP5001: This assertion might not hold.
+ Passification.bpl(41,1): A
+Passification.bpl(118,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(106,1): L0
- Passification.bpl(111,1): L1
- Passification.bpl(115,1): L2
-Passification.bpl(151,3): Error BP5001: This assertion might not hold.
+ Passification.bpl(108,1): L0
+ Passification.bpl(113,1): L1
+ Passification.bpl(117,1): L2
+Passification.bpl(153,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(144,1): L0
- Passification.bpl(150,1): L2
-Passification.bpl(165,3): Error BP5001: This assertion might not hold.
+ Passification.bpl(146,1): L0
+ Passification.bpl(152,1): L2
+Passification.bpl(167,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(158,1): L0
- Passification.bpl(161,1): L1
- Passification.bpl(164,1): L2
+ Passification.bpl(160,1): L0
+ Passification.bpl(163,1): L1
+ Passification.bpl(166,1): L2
Boogie program verifier finished with 7 verified, 4 errors
@@ -44,121 +44,121 @@ Boogie program verifier finished with 7 verified, 4 errors
Boogie program verifier finished with 4 verified, 0 errors
-------------------- Ensures.bpl --------------------
-Ensures.bpl(30,5): Error BP5003: A postcondition might not hold on this return path.
-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
+Ensures.bpl(32,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(28,3): start
-Ensures.bpl(35,5): Error BP5003: A postcondition might not hold on this return path.
-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
+ Ensures.bpl(30,3): start
+Ensures.bpl(37,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(34,3): start
-Ensures.bpl(41,5): Error BP5003: A postcondition might not hold on this return path.
-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
+ Ensures.bpl(36,3): start
+Ensures.bpl(43,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(39,3): start
-Ensures.bpl(47,5): Error BP5003: A postcondition might not hold on this return path.
-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
+ Ensures.bpl(41,3): start
+Ensures.bpl(49,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(45,3): start
-Ensures.bpl(72,5): Error BP5003: A postcondition might not hold on this return path.
-Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
+ Ensures.bpl(47,3): start
+Ensures.bpl(74,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(70,3): start
+ Ensures.bpl(72,3): start
Boogie program verifier finished with 5 verified, 5 errors
-------------------- Old.bpl --------------------
-Old.bpl(29,5): Error BP5003: A postcondition might not hold on this return path.
-Old.bpl(26,3): Related location: This is the postcondition that might not hold.
+Old.bpl(31,5): Error BP5003: A postcondition might not hold on this return path.
+Old.bpl(28,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Old.bpl(28,3): start
+ Old.bpl(30,3): start
Boogie program verifier finished with 7 verified, 1 error
-------------------- OldIllegal.bpl --------------------
-OldIllegal.bpl(7,11): Error: old expressions allowed only in two-state contexts
-OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts
+OldIllegal.bpl(9,11): Error: old expressions allowed only in two-state contexts
+OldIllegal.bpl(16,23): Error: old expressions allowed only in two-state contexts
2 name resolution errors detected in OldIllegal.bpl
-------------------- Arrays.bpl --------------------
-Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
+Arrays.bpl(48,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(40,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(42,3): start
-Arrays.bpl(127,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
+ Arrays.bpl(44,3): start
+Arrays.bpl(129,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(121,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(123,3): start
+ Arrays.bpl(125,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Axioms.bpl --------------------
-Axioms.bpl(19,5): Error BP5001: This assertion might not hold.
+Axioms.bpl(21,5): Error BP5001: This assertion might not hold.
Execution trace:
- Axioms.bpl(18,3): start
+ Axioms.bpl(20,3): start
Boogie program verifier finished with 2 verified, 1 error
-------------------- Quantifiers.bpl --------------------
-Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold.
+Quantifiers.bpl(22,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(19,3): start
-Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold.
+ Quantifiers.bpl(21,3): start
+Quantifiers.bpl(45,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(42,3): start
-Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold.
+ Quantifiers.bpl(44,3): start
+Quantifiers.bpl(67,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(64,3): start
-Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold.
+ Quantifiers.bpl(66,3): start
+Quantifiers.bpl(75,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(71,3): start
-Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold.
+ Quantifiers.bpl(73,3): start
+Quantifiers.bpl(127,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(124,3): start
-Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold.
+ Quantifiers.bpl(126,3): start
+Quantifiers.bpl(152,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(149,3): start
+ Quantifiers.bpl(151,3): start
Boogie program verifier finished with 8 verified, 6 errors
-------------------- Call.bpl --------------------
-Call.bpl(13,5): Error BP5001: This assertion might not hold.
+Call.bpl(15,5): Error BP5001: This assertion might not hold.
Execution trace:
- Call.bpl(9,3): entry
-Call.bpl(46,5): Error BP5001: This assertion might not hold.
+ Call.bpl(11,3): entry
+Call.bpl(48,5): Error BP5001: This assertion might not hold.
Execution trace:
- Call.bpl(45,3): start
-Call.bpl(55,5): Error BP5003: A postcondition might not hold on this return path.
-Call.bpl(20,3): Related location: This is the postcondition that might not hold.
+ Call.bpl(47,3): start
+Call.bpl(57,5): Error BP5003: A postcondition might not hold on this return path.
+Call.bpl(22,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Call.bpl(53,3): start
+ Call.bpl(55,3): start
Boogie program verifier finished with 2 verified, 3 errors
-------------------- AssumeEnsures.bpl --------------------
-AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold.
+AssumeEnsures.bpl(30,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(26,5): entry
-AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold.
+ AssumeEnsures.bpl(28,5): entry
+AssumeEnsures.bpl(49,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(46,5): entry
-AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold.
+ AssumeEnsures.bpl(48,5): entry
+AssumeEnsures.bpl(64,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(60,5): entry
+ AssumeEnsures.bpl(62,5): entry
Boogie program verifier finished with 4 verified, 3 errors
-------------------- CutBackEdge.bpl --------------------
-CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained by the loop.
+CutBackEdge.bpl(12,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- CutBackEdge.bpl(5,3): entry
- CutBackEdge.bpl(9,3): block850
-CutBackEdge.bpl(20,5): Error BP5004: This loop invariant might not hold on entry.
+ CutBackEdge.bpl(7,3): entry
+ CutBackEdge.bpl(11,3): block850
+CutBackEdge.bpl(22,5): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
-CutBackEdge.bpl(26,5): Error BP5001: This assertion might not hold.
+CutBackEdge.bpl(28,5): Error BP5001: This assertion might not hold.
Execution trace:
- CutBackEdge.bpl(25,3): L
-CutBackEdge.bpl(38,5): Error BP5004: This loop invariant might not hold on entry.
+ CutBackEdge.bpl(27,3): L
+CutBackEdge.bpl(40,5): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
Boogie program verifier finished with 1 verified, 4 errors
@@ -168,310 +168,310 @@ Boogie program verifier finished with 1 verified, 4 errors
Boogie program verifier finished with 2 verified, 0 errors
-------------------- LoopInvAssume.bpl --------------------
-LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold.
+LoopInvAssume.bpl(20,7): Error BP5001: This assertion might not hold.
Execution trace:
- LoopInvAssume.bpl(8,4): entry
- LoopInvAssume.bpl(16,4): exit
+ LoopInvAssume.bpl(10,4): entry
+ LoopInvAssume.bpl(18,4): exit
Boogie program verifier finished with 0 verified, 1 error
-------------------- strings-no-where.bpl --------------------
-strings-no-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator ==
-strings-no-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator ==
-strings-no-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)
-strings-no-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
-strings-no-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)
-strings-no-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
-strings-no-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
-strings-no-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator ==
-strings-no-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator ==
-strings-no-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)
-strings-no-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-no-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-no-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-no-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-no-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator ==
-strings-no-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator ==
-strings-no-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any)
-strings-no-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)
+strings-no-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-no-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)
+strings-no-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-no-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-no-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)
+strings-no-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any)
+strings-no-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator ==
18 type checking errors detected in strings-no-where.bpl
-------------------- strings-where.bpl --------------------
-strings-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator ==
-strings-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator ==
-strings-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)
-strings-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
-strings-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)
-strings-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
-strings-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
-strings-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator ==
-strings-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator ==
-strings-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)
-strings-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any)
-strings-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator ==
-strings-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator ==
-strings-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any)
-strings-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)
+strings-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)
+strings-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)
+strings-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any)
+strings-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator ==
18 type checking errors detected in strings-where.bpl
-------------------- Structured.bpl --------------------
-Structured.bpl(252,14): Error BP5003: A postcondition might not hold on this return path.
-Structured.bpl(243,3): Related location: This is the postcondition that might not hold.
+Structured.bpl(254,14): Error BP5003: A postcondition might not hold on this return path.
+Structured.bpl(245,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Structured.bpl(244,5): anon0
- Structured.bpl(246,5): anon6_LoopBody
- Structured.bpl(247,7): anon7_LoopBody
- Structured.bpl(248,11): anon8_Then
- Structured.bpl(252,14): anon9_Then
-Structured.bpl(303,3): Error BP5001: This assertion might not hold.
+ Structured.bpl(246,5): anon0
+ Structured.bpl(248,5): anon6_LoopBody
+ Structured.bpl(249,7): anon7_LoopBody
+ Structured.bpl(250,11): anon8_Then
+ Structured.bpl(254,14): anon9_Then
+Structured.bpl(305,3): Error BP5001: This assertion might not hold.
Execution trace:
- Structured.bpl(299,5): anon0
- Structured.bpl(300,3): anon3_Else
- Structured.bpl(303,3): anon2
-Structured.bpl(311,7): Error BP5001: This assertion might not hold.
+ Structured.bpl(301,5): anon0
+ Structured.bpl(302,3): anon3_Else
+ Structured.bpl(305,3): anon2
+Structured.bpl(313,7): Error BP5001: This assertion might not hold.
Execution trace:
- Structured.bpl(308,3): anon0
- Structured.bpl(308,3): anon1_Then
- Structured.bpl(309,5): A
+ Structured.bpl(310,3): anon0
+ Structured.bpl(310,3): anon1_Then
+ Structured.bpl(311,5): A
Boogie program verifier finished with 16 verified, 3 errors
-------------------- Where.bpl --------------------
-Where.bpl(8,3): Error BP5001: This assertion might not hold.
+Where.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(6,3): anon0
-Where.bpl(22,3): Error BP5001: This assertion might not hold.
+ Where.bpl(8,3): anon0
+Where.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(16,5): anon0
-Where.bpl(32,3): Error BP5001: This assertion might not hold.
+ Where.bpl(18,5): anon0
+Where.bpl(34,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(30,3): anon0
-Where.bpl(44,3): Error BP5001: This assertion might not hold.
+ Where.bpl(32,3): anon0
+Where.bpl(46,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(40,5): anon0
-Where.bpl(57,3): Error BP5001: This assertion might not hold.
+ Where.bpl(42,5): anon0
+Where.bpl(59,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(52,3): anon0
-Where.bpl(111,3): Error BP5001: This assertion might not hold.
+ Where.bpl(54,3): anon0
+Where.bpl(113,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(102,5): anon0
- Where.bpl(104,3): anon3_LoopHead
- Where.bpl(104,3): anon3_LoopDone
-Where.bpl(128,3): Error BP5001: This assertion might not hold.
+ Where.bpl(104,5): anon0
+ Where.bpl(106,3): anon3_LoopHead
+ Where.bpl(106,3): anon3_LoopDone
+Where.bpl(130,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(121,5): anon0
- Where.bpl(122,3): anon3_LoopHead
- Where.bpl(122,3): anon3_LoopDone
-Where.bpl(145,3): Error BP5001: This assertion might not hold.
+ Where.bpl(123,5): anon0
+ Where.bpl(124,3): anon3_LoopHead
+ Where.bpl(124,3): anon3_LoopDone
+Where.bpl(147,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(138,5): anon0
- Where.bpl(139,3): anon3_LoopHead
- Where.bpl(139,3): anon3_LoopDone
-Where.bpl(162,3): Error BP5001: This assertion might not hold.
+ Where.bpl(140,5): anon0
+ Where.bpl(141,3): anon3_LoopHead
+ Where.bpl(141,3): anon3_LoopDone
+Where.bpl(164,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(155,5): anon0
- Where.bpl(156,3): anon3_LoopHead
- Where.bpl(156,3): anon3_LoopDone
+ Where.bpl(157,5): anon0
+ Where.bpl(158,3): anon3_LoopHead
+ Where.bpl(158,3): anon3_LoopDone
Boogie program verifier finished with 2 verified, 9 errors
-------------------- UpdateExpr.bpl --------------------
-UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold.
+UpdateExpr.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(14,3): anon0
-UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold.
+ UpdateExpr.bpl(16,3): anon0
+UpdateExpr.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(19,3): anon0
-UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold.
+ UpdateExpr.bpl(21,3): anon0
+UpdateExpr.bpl(34,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(32,3): anon0
-UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold.
+ UpdateExpr.bpl(34,3): anon0
+UpdateExpr.bpl(40,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(38,3): anon0
-UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold.
+ UpdateExpr.bpl(40,3): anon0
+UpdateExpr.bpl(54,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(51,5): anon0
+ UpdateExpr.bpl(53,5): anon0
Boogie program verifier finished with 5 verified, 5 errors
-------------------- NeverPattern.bpl --------------------
-NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold.
+NeverPattern.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(15,3): anon0
-NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold.
+ NeverPattern.bpl(17,3): anon0
+NeverPattern.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(21,3): anon0
-NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.
+ NeverPattern.bpl(23,3): anon0
+NeverPattern.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(27,3): anon0
+ NeverPattern.bpl(29,3): anon0
Boogie program verifier finished with 2 verified, 3 errors
-------------------- NullaryMaps.bpl --------------------
-NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.
-Execution trace:
- NullaryMaps.bpl(28,3): anon0
NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(28,3): anon0
-NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold.
+ NullaryMaps.bpl(30,3): anon0
+NullaryMaps.bpl(32,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NullaryMaps.bpl(30,3): anon0
+NullaryMaps.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(36,3): anon0
+ NullaryMaps.bpl(38,3): anon0
Boogie program verifier finished with 2 verified, 3 errors
-------------------- Implies.bpl --------------------
-Implies.bpl(12,3): Error BP5001: This assertion might not hold.
+Implies.bpl(14,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(11,3): anon0
-Implies.bpl(15,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(13,3): anon0
+Implies.bpl(17,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(11,3): anon0
-Implies.bpl(19,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(13,3): anon0
+Implies.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(19,3): anon0
-Implies.bpl(24,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(21,3): anon0
+Implies.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(24,3): anon0
-Implies.bpl(25,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(26,3): anon0
+Implies.bpl(27,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(24,3): anon0
-Implies.bpl(29,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(26,3): anon0
+Implies.bpl(31,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(29,3): anon0
-Implies.bpl(34,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(31,3): anon0
+Implies.bpl(36,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(34,3): anon0
-Implies.bpl(35,3): Error BP5001: This assertion might not hold.
+ Implies.bpl(36,3): anon0
+Implies.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(34,3): anon0
+ Implies.bpl(36,3): anon0
Boogie program verifier finished with 0 verified, 8 errors
-------------------- IfThenElse1.bpl --------------------
-IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.
+IfThenElse1.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- IfThenElse1.bpl(26,3): anon0
-IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.
+ IfThenElse1.bpl(28,3): anon0
+IfThenElse1.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- IfThenElse1.bpl(33,3): anon0
+ IfThenElse1.bpl(35,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
-------------------- Lambda.bpl --------------------
-Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
+Lambda.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
-Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
+ Lambda.bpl(38,5): anon0
+Lambda.bpl(40,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(38,5): anon0
Boogie program verifier finished with 6 verified, 2 errors
-------------------- LambdaPoly.bpl --------------------
-LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
+LambdaPoly.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- LambdaPoly.bpl(24,5): anon0
- LambdaPoly.bpl(27,5): anon4_Then
-LambdaPoly.bpl(31,5): Error BP5001: This assertion might not hold.
+ LambdaPoly.bpl(26,5): anon0
+ LambdaPoly.bpl(29,5): anon4_Then
+LambdaPoly.bpl(33,5): Error BP5001: This assertion might not hold.
Execution trace:
- LambdaPoly.bpl(24,5): anon0
- LambdaPoly.bpl(30,5): anon5_Then
-LambdaPoly.bpl(36,5): Error BP5001: This assertion might not hold.
+ LambdaPoly.bpl(26,5): anon0
+ LambdaPoly.bpl(32,5): anon5_Then
+LambdaPoly.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
- LambdaPoly.bpl(24,5): anon0
- LambdaPoly.bpl(34,5): anon5_Else
+ LambdaPoly.bpl(26,5): anon0
+ LambdaPoly.bpl(36,5): anon5_Else
Boogie program verifier finished with 1 verified, 3 errors
-------------------- LambdaOldExpressions.bpl --------------------
-LambdaOldExpressions.bpl(27,1): Error BP5003: A postcondition might not hold on this return path.
-LambdaOldExpressions.bpl(21,3): Related location: This is the postcondition that might not hold.
+LambdaOldExpressions.bpl(29,1): Error BP5003: A postcondition might not hold on this return path.
+LambdaOldExpressions.bpl(23,3): Related location: This is the postcondition that might not hold.
Execution trace:
- LambdaOldExpressions.bpl(25,7): anon0
+ LambdaOldExpressions.bpl(27,7): anon0
Boogie program verifier finished with 4 verified, 1 error
-------------------- SelectiveChecking.bpl --------------------
-SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.
-Execution trace:
- SelectiveChecking.bpl(15,3): anon0
-SelectiveChecking.bpl(30,3): Error BP5001: This assertion might not hold.
+SelectiveChecking.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- SelectiveChecking.bpl(24,3): anon0
- SelectiveChecking.bpl(27,5): anon3_Then
- SelectiveChecking.bpl(30,3): anon2
-SelectiveChecking.bpl(37,3): Error BP5001: This assertion might not hold.
+ SelectiveChecking.bpl(17,3): anon0
+SelectiveChecking.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- SelectiveChecking.bpl(37,3): anon0
+ SelectiveChecking.bpl(26,3): anon0
+ SelectiveChecking.bpl(29,5): anon3_Then
+ SelectiveChecking.bpl(32,3): anon2
SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- SelectiveChecking.bpl(37,3): anon0
+ SelectiveChecking.bpl(39,3): anon0
+SelectiveChecking.bpl(41,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(39,3): anon0
Boogie program verifier finished with 1 verified, 4 errors
-------------------- FreeCall.bpl --------------------
-FreeCall.bpl(37,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(39,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(10,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(39,5): anon0
+FreeCall.bpl(44,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(8,3): Related location: This is the precondition that might not hold.
Execution trace:
- FreeCall.bpl(37,5): anon0
-FreeCall.bpl(42,5): Error BP5002: A precondition for this call might not hold.
-FreeCall.bpl(6,3): Related location: This is the precondition that might not hold.
+ FreeCall.bpl(44,5): anon0
+FreeCall.bpl(61,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(18,3): Related location: This is the precondition that might not hold.
Execution trace:
- FreeCall.bpl(42,5): anon0
-FreeCall.bpl(59,5): Error BP5002: A precondition for this call might not hold.
+ FreeCall.bpl(61,5): anon0
+FreeCall.bpl(68,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(16,3): Related location: This is the precondition that might not hold.
Execution trace:
- FreeCall.bpl(59,5): anon0
-FreeCall.bpl(66,5): Error BP5002: A precondition for this call might not hold.
-FreeCall.bpl(14,3): Related location: This is the precondition that might not hold.
-Execution trace:
- FreeCall.bpl(66,5): anon0
+ FreeCall.bpl(68,5): anon0
Boogie program verifier finished with 7 verified, 4 errors
-------------------- AssumptionVariables0.bpl --------------------
-AssumptionVariables0.bpl(15,5): Error BP5001: This assertion might not hold.
+AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
Execution trace:
- AssumptionVariables0.bpl(13,8): anon0
-AssumptionVariables0.bpl(25,5): Error BP5001: This assertion might not hold.
+ AssumptionVariables0.bpl(15,8): anon0
+AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
Execution trace:
- AssumptionVariables0.bpl(23,5): anon0
-AssumptionVariables0.bpl(37,5): Error BP5001: This assertion might not hold.
+ AssumptionVariables0.bpl(25,5): anon0
+AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
Execution trace:
- AssumptionVariables0.bpl(35,8): anon0
+ AssumptionVariables0.bpl(37,8): anon0
Boogie program verifier finished with 1 verified, 3 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
-Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
+Arrays.bpl(48,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(40,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(42,3): start
-Arrays.bpl(127,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
+ Arrays.bpl(44,3): start
+Arrays.bpl(129,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(121,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(123,3): start
+ Arrays.bpl(125,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Lambda.bpl /typeEncoding:m --------------------
-Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
+Lambda.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
-Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
+ Lambda.bpl(38,5): anon0
+Lambda.bpl(40,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(38,5): anon0
Boogie program verifier finished with 6 verified, 2 errors
-------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
-TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
+TypeEncodingM.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- TypeEncodingM.bpl(11,9): anon0
+ TypeEncodingM.bpl(13,9): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- sk_hack.bpl --------------------
@@ -479,65 +479,65 @@ Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
-------------------- ContractEvaluationOrder.bpl --------------------
-ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path.
-ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
+ContractEvaluationOrder.bpl(10,1): Error BP5003: A postcondition might not hold on this return path.
+ContractEvaluationOrder.bpl(5,3): Related location: This is the postcondition that might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(7,5): anon0
-ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold.
+ ContractEvaluationOrder.bpl(9,5): anon0
+ContractEvaluationOrder.bpl(17,3): Error BP5001: This assertion might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(12,5): anon0
-ContractEvaluationOrder.bpl(24,3): Error BP5002: A precondition for this call might not hold.
-ContractEvaluationOrder.bpl(30,3): Related location: This is the precondition that might not hold.
+ ContractEvaluationOrder.bpl(14,5): anon0
+ContractEvaluationOrder.bpl(26,3): Error BP5002: A precondition for this call might not hold.
+ContractEvaluationOrder.bpl(32,3): Related location: This is the precondition that might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(23,5): anon0
+ ContractEvaluationOrder.bpl(25,5): anon0
Boogie program verifier finished with 1 verified, 3 errors
-------------------- Timeouts0.bpl --------------------
-Timeouts0.bpl(19,5): Error BP5003: A postcondition might not hold on this return path.
-Timeouts0.bpl(4,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- Timeouts0.bpl(8,7): anon0
- Timeouts0.bpl(10,5): anon4_LoopHead
- Timeouts0.bpl(10,5): anon4_LoopDone
- Timeouts0.bpl(19,5): anon5_LoopHead
- Timeouts0.bpl(19,5): anon5_LoopDone
-Timeouts0.bpl(21,7): Error BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
- Timeouts0.bpl(8,7): anon0
- Timeouts0.bpl(10,5): anon4_LoopHead
- Timeouts0.bpl(10,5): anon4_LoopDone
- Timeouts0.bpl(19,5): anon5_LoopHead
- Timeouts0.bpl(23,11): anon5_LoopBody
-Timeouts0.bpl(48,5): Error BP5003: A postcondition might not hold on this return path.
-Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- Timeouts0.bpl(37,7): anon0
- Timeouts0.bpl(39,5): anon4_LoopHead
- Timeouts0.bpl(39,5): anon4_LoopDone
- Timeouts0.bpl(48,5): anon5_LoopHead
- Timeouts0.bpl(48,5): anon5_LoopDone
-Timeouts0.bpl(50,7): Error BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
- Timeouts0.bpl(37,7): anon0
- Timeouts0.bpl(39,5): anon4_LoopHead
- Timeouts0.bpl(39,5): anon4_LoopDone
- Timeouts0.bpl(48,5): anon5_LoopHead
- Timeouts0.bpl(52,11): anon5_LoopBody
-Timeouts0.bpl(77,5): Error BP5003: A postcondition might not hold on this return path.
-Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- Timeouts0.bpl(66,7): anon0
- Timeouts0.bpl(68,5): anon4_LoopHead
- Timeouts0.bpl(68,5): anon4_LoopDone
- Timeouts0.bpl(77,5): anon5_LoopHead
- Timeouts0.bpl(77,5): anon5_LoopDone
-Timeouts0.bpl(79,7): Error BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
- Timeouts0.bpl(66,7): anon0
- Timeouts0.bpl(68,5): anon4_LoopHead
- Timeouts0.bpl(68,5): anon4_LoopDone
- Timeouts0.bpl(77,5): anon5_LoopHead
- Timeouts0.bpl(81,11): anon5_LoopBody
+Timeouts0.bpl(21,5): Error BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(6,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(10,7): anon0
+ Timeouts0.bpl(12,5): anon4_LoopHead
+ Timeouts0.bpl(12,5): anon4_LoopDone
+ Timeouts0.bpl(21,5): anon5_LoopHead
+ Timeouts0.bpl(21,5): anon5_LoopDone
+Timeouts0.bpl(23,7): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(10,7): anon0
+ Timeouts0.bpl(12,5): anon4_LoopHead
+ Timeouts0.bpl(12,5): anon4_LoopDone
+ Timeouts0.bpl(21,5): anon5_LoopHead
+ Timeouts0.bpl(25,11): anon5_LoopBody
+Timeouts0.bpl(50,5): Error BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(33,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(39,7): anon0
+ Timeouts0.bpl(41,5): anon4_LoopHead
+ Timeouts0.bpl(41,5): anon4_LoopDone
+ Timeouts0.bpl(50,5): anon5_LoopHead
+ Timeouts0.bpl(50,5): anon5_LoopDone
+Timeouts0.bpl(52,7): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(39,7): anon0
+ Timeouts0.bpl(41,5): anon4_LoopHead
+ Timeouts0.bpl(41,5): anon4_LoopDone
+ Timeouts0.bpl(50,5): anon5_LoopHead
+ Timeouts0.bpl(54,11): anon5_LoopBody
+Timeouts0.bpl(79,5): Error BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(62,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(68,7): anon0
+ Timeouts0.bpl(70,5): anon4_LoopHead
+ Timeouts0.bpl(70,5): anon4_LoopDone
+ Timeouts0.bpl(79,5): anon5_LoopHead
+ Timeouts0.bpl(79,5): anon5_LoopDone
+Timeouts0.bpl(81,7): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(68,7): anon0
+ Timeouts0.bpl(70,5): anon4_LoopHead
+ Timeouts0.bpl(70,5): anon4_LoopDone
+ Timeouts0.bpl(79,5): anon5_LoopHead
+ Timeouts0.bpl(83,11): anon5_LoopBody
Boogie program verifier finished with 0 verified, 6 errors
diff --git a/Test/test2/Arrays.bpl b/Test/test2/Arrays.bpl
index d0f712c9..f153b599 100644
--- a/Test/test2/Arrays.bpl
+++ b/Test/test2/Arrays.bpl
@@ -1,3 +1,7 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m %s > %t
+// RUN: %diff %s.expect %t
// -------------------- 1-dimensional arrays --------------------
var A: [ref]int;
diff --git a/Test/test2/Arrays.bpl.expect b/Test/test2/Arrays.bpl.expect
new file mode 100644
index 00000000..34804dc0
--- /dev/null
+++ b/Test/test2/Arrays.bpl.expect
@@ -0,0 +1,10 @@
+Arrays.bpl(50,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(42,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Arrays.bpl(46,3): start
+Arrays.bpl(131,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(123,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Arrays.bpl(127,3): start
+
+Boogie program verifier finished with 8 verified, 2 errors
diff --git a/Test/test2/AssumeEnsures.bpl b/Test/test2/AssumeEnsures.bpl
index 901c06c8..9c19e5bc 100644
--- a/Test/test2/AssumeEnsures.bpl
+++ b/Test/test2/AssumeEnsures.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var g: int;
procedure Foo() returns ();
diff --git a/Test/test2/AssumeEnsures.bpl.expect b/Test/test2/AssumeEnsures.bpl.expect
new file mode 100644
index 00000000..7a65cace
--- /dev/null
+++ b/Test/test2/AssumeEnsures.bpl.expect
@@ -0,0 +1,11 @@
+AssumeEnsures.bpl(30,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumeEnsures.bpl(28,5): entry
+AssumeEnsures.bpl(49,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumeEnsures.bpl(48,5): entry
+AssumeEnsures.bpl(64,9): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumeEnsures.bpl(62,5): entry
+
+Boogie program verifier finished with 4 verified, 3 errors
diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl
index 96537c0d..e1800d3d 100644
--- a/Test/test2/AssumptionVariables0.bpl
+++ b/Test/test2/AssumptionVariables0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure Test0()
{
var {:assumption} a0: bool;
diff --git a/Test/test2/AssumptionVariables0.bpl.expect b/Test/test2/AssumptionVariables0.bpl.expect
new file mode 100644
index 00000000..54ddb2a9
--- /dev/null
+++ b/Test/test2/AssumptionVariables0.bpl.expect
@@ -0,0 +1,11 @@
+AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumptionVariables0.bpl(15,8): anon0
+AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumptionVariables0.bpl(25,5): anon0
+AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ AssumptionVariables0.bpl(37,8): anon0
+
+Boogie program verifier finished with 1 verified, 3 errors
diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl
index 4fe7a8a7..0da46116 100644
--- a/Test/test2/Axioms.bpl
+++ b/Test/test2/Axioms.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
const Seven: int;
axiom Seven == 7;
diff --git a/Test/test2/Axioms.bpl.expect b/Test/test2/Axioms.bpl.expect
new file mode 100644
index 00000000..2557ee13
--- /dev/null
+++ b/Test/test2/Axioms.bpl.expect
@@ -0,0 +1,5 @@
+Axioms.bpl(21,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Axioms.bpl(20,3): start
+
+Boogie program verifier finished with 2 verified, 1 error
diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl
index 553d5002..f68dbb26 100644
--- a/Test/test2/B.bpl
+++ b/Test/test2/B.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// ----------- BEGIN PRELUDE
var Heap: [ref, name]int;
diff --git a/Test/test2/B.bpl.expect b/Test/test2/B.bpl.expect
new file mode 100644
index 00000000..00ddb38b
--- /dev/null
+++ b/Test/test2/B.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/test2/Call.bpl b/Test/test2/Call.bpl
index c1de1e71..02902b0a 100644
--- a/Test/test2/Call.bpl
+++ b/Test/test2/Call.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure Bar() returns (barresult: ref);
procedure Foo();
diff --git a/Test/test2/Call.bpl.expect b/Test/test2/Call.bpl.expect
new file mode 100644
index 00000000..934b3ac5
--- /dev/null
+++ b/Test/test2/Call.bpl.expect
@@ -0,0 +1,12 @@
+Call.bpl(15,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Call.bpl(11,3): entry
+Call.bpl(48,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Call.bpl(47,3): start
+Call.bpl(57,5): Error BP5003: A postcondition might not hold on this return path.
+Call.bpl(22,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Call.bpl(55,3): start
+
+Boogie program verifier finished with 2 verified, 3 errors
diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl
index 3eab4bda..445b84c6 100644
--- a/Test/test2/ContractEvaluationOrder.bpl
+++ b/Test/test2/ContractEvaluationOrder.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
procedure P() returns (x, y: int)
ensures x == y; // ensured by the body
ensures x == 0; // error: not ensured by the body
diff --git a/Test/test2/ContractEvaluationOrder.bpl.expect b/Test/test2/ContractEvaluationOrder.bpl.expect
new file mode 100644
index 00000000..4bab4b21
--- /dev/null
+++ b/Test/test2/ContractEvaluationOrder.bpl.expect
@@ -0,0 +1,13 @@
+ContractEvaluationOrder.bpl(10,1): Error BP5003: A postcondition might not hold on this return path.
+ContractEvaluationOrder.bpl(5,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ ContractEvaluationOrder.bpl(9,5): anon0
+ContractEvaluationOrder.bpl(17,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ ContractEvaluationOrder.bpl(14,5): anon0
+ContractEvaluationOrder.bpl(26,3): Error BP5002: A precondition for this call might not hold.
+ContractEvaluationOrder.bpl(32,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ ContractEvaluationOrder.bpl(25,5): anon0
+
+Boogie program verifier finished with 1 verified, 3 errors
diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl
index 7294d0f9..c1d08216 100644
--- a/Test/test2/CutBackEdge.bpl
+++ b/Test/test2/CutBackEdge.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure Test()
{
var i: int;
diff --git a/Test/test2/CutBackEdge.bpl.expect b/Test/test2/CutBackEdge.bpl.expect
new file mode 100644
index 00000000..90719e35
--- /dev/null
+++ b/Test/test2/CutBackEdge.bpl.expect
@@ -0,0 +1,13 @@
+CutBackEdge.bpl(12,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ CutBackEdge.bpl(7,3): entry
+ CutBackEdge.bpl(11,3): block850
+CutBackEdge.bpl(22,5): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+CutBackEdge.bpl(28,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ CutBackEdge.bpl(27,3): L
+CutBackEdge.bpl(40,5): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+
+Boogie program verifier finished with 1 verified, 4 errors
diff --git a/Test/test2/Ensures.bpl b/Test/test2/Ensures.bpl
index 4e36c108..8996d100 100644
--- a/Test/test2/Ensures.bpl
+++ b/Test/test2/Ensures.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var H: [ref,name]int;
var that: ref;
diff --git a/Test/test2/Ensures.bpl.expect b/Test/test2/Ensures.bpl.expect
new file mode 100644
index 00000000..28917250
--- /dev/null
+++ b/Test/test2/Ensures.bpl.expect
@@ -0,0 +1,22 @@
+Ensures.bpl(32,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Ensures.bpl(30,3): start
+Ensures.bpl(37,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Ensures.bpl(36,3): start
+Ensures.bpl(43,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Ensures.bpl(41,3): start
+Ensures.bpl(49,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Ensures.bpl(47,3): start
+Ensures.bpl(74,5): Error BP5003: A postcondition might not hold on this return path.
+Ensures.bpl(21,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Ensures.bpl(72,3): start
+
+Boogie program verifier finished with 5 verified, 5 errors
diff --git a/Test/test2/False.bpl b/Test/test2/False.bpl
index 3fe14865..5399b024 100644
--- a/Test/test2/False.bpl
+++ b/Test/test2/False.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure Test1()
{
entry:
diff --git a/Test/test2/False.bpl.expect b/Test/test2/False.bpl.expect
new file mode 100644
index 00000000..41374b00
--- /dev/null
+++ b/Test/test2/False.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/test2/FormulaTerm.bpl b/Test/test2/FormulaTerm.bpl
index e14707cb..b36f971b 100644
--- a/Test/test2/FormulaTerm.bpl
+++ b/Test/test2/FormulaTerm.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// Test formula-term distinction in Simplify
procedure plus(x: int, y: int) returns (z: int);
diff --git a/Test/test2/FormulaTerm.bpl.expect b/Test/test2/FormulaTerm.bpl.expect
new file mode 100644
index 00000000..70fe60b3
--- /dev/null
+++ b/Test/test2/FormulaTerm.bpl.expect
@@ -0,0 +1,6 @@
+FormulaTerm.bpl(12,3): Error BP5003: A postcondition might not hold on this return path.
+FormulaTerm.bpl(6,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ FormulaTerm.bpl(10,1): start
+
+Boogie program verifier finished with 11 verified, 1 error
diff --git a/Test/test2/FormulaTerm2.bpl b/Test/test2/FormulaTerm2.bpl
index 6c5e4bf3..881a6222 100644
--- a/Test/test2/FormulaTerm2.bpl
+++ b/Test/test2/FormulaTerm2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// This file has been created to test some of the formula/term issues in Zap.
// However, the test harness does not specify any particular prover to be used,
// since these tests should pass regardless of which prover is used.
diff --git a/Test/test2/FormulaTerm2.bpl.expect b/Test/test2/FormulaTerm2.bpl.expect
new file mode 100644
index 00000000..aa959a1d
--- /dev/null
+++ b/Test/test2/FormulaTerm2.bpl.expect
@@ -0,0 +1,8 @@
+FormulaTerm2.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ FormulaTerm2.bpl(38,3): start
+FormulaTerm2.bpl(49,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ FormulaTerm2.bpl(47,3): start
+
+Boogie program verifier finished with 2 verified, 2 errors
diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl
index a873a4e6..aaaba3ac 100644
--- a/Test/test2/FreeCall.bpl
+++ b/Test/test2/FreeCall.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// Test the implementation of free calls. These calls don't check the preconditions of the
// called procedure in the caller.
diff --git a/Test/test2/FreeCall.bpl.expect b/Test/test2/FreeCall.bpl.expect
new file mode 100644
index 00000000..edcfee63
--- /dev/null
+++ b/Test/test2/FreeCall.bpl.expect
@@ -0,0 +1,18 @@
+FreeCall.bpl(39,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(10,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(39,5): anon0
+FreeCall.bpl(44,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(8,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(44,5): anon0
+FreeCall.bpl(61,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(18,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(61,5): anon0
+FreeCall.bpl(68,5): Error BP5002: A precondition for this call might not hold.
+FreeCall.bpl(16,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ FreeCall.bpl(68,5): anon0
+
+Boogie program verifier finished with 7 verified, 4 errors
diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl
index 8a867f50..4c79ce8b 100644
--- a/Test/test2/IfThenElse1.bpl
+++ b/Test/test2/IfThenElse1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
type t1;
procedure ok()
diff --git a/Test/test2/IfThenElse1.bpl.expect b/Test/test2/IfThenElse1.bpl.expect
new file mode 100644
index 00000000..48386461
--- /dev/null
+++ b/Test/test2/IfThenElse1.bpl.expect
@@ -0,0 +1,8 @@
+IfThenElse1.bpl(28,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ IfThenElse1.bpl(28,3): anon0
+IfThenElse1.bpl(35,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ IfThenElse1.bpl(35,3): anon0
+
+Boogie program verifier finished with 2 verified, 2 errors
diff --git a/Test/test2/Implies.bpl b/Test/test2/Implies.bpl
index f20b0450..05a3e5fe 100644
--- a/Test/test2/Implies.bpl
+++ b/Test/test2/Implies.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
const a:bool;
const b:bool;
diff --git a/Test/test2/Implies.bpl.expect b/Test/test2/Implies.bpl.expect
new file mode 100644
index 00000000..93e83ffd
--- /dev/null
+++ b/Test/test2/Implies.bpl.expect
@@ -0,0 +1,26 @@
+Implies.bpl(14,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(13,3): anon0
+Implies.bpl(17,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(13,3): anon0
+Implies.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(21,3): anon0
+Implies.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(26,3): anon0
+Implies.bpl(27,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(26,3): anon0
+Implies.bpl(31,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(31,3): anon0
+Implies.bpl(36,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(36,3): anon0
+Implies.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Implies.bpl(36,3): anon0
+
+Boogie program verifier finished with 0 verified, 8 errors
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
index 68c83d43..cbcbd334 100644
--- a/Test/test2/Lambda.bpl
+++ b/Test/test2/Lambda.bpl
@@ -1,3 +1,7 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
+// RUN: %boogie -noinfer -typeEncoding:m %s > %t
+// RUN: %diff %s.expect %t
procedure foo()
{
var a: [int]int;
diff --git a/Test/test2/Lambda.bpl.expect b/Test/test2/Lambda.bpl.expect
new file mode 100644
index 00000000..d45375fa
--- /dev/null
+++ b/Test/test2/Lambda.bpl.expect
@@ -0,0 +1,8 @@
+Lambda.bpl(41,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Lambda.bpl(40,5): anon0
+Lambda.bpl(42,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Lambda.bpl(40,5): anon0
+
+Boogie program verifier finished with 6 verified, 2 errors
diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl
index 9f17245f..94a6e520 100644
--- a/Test/test2/LambdaOldExpressions.bpl
+++ b/Test/test2/LambdaOldExpressions.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var b: bool;
diff --git a/Test/test2/LambdaOldExpressions.bpl.expect b/Test/test2/LambdaOldExpressions.bpl.expect
new file mode 100644
index 00000000..1268eb7e
--- /dev/null
+++ b/Test/test2/LambdaOldExpressions.bpl.expect
@@ -0,0 +1,6 @@
+LambdaOldExpressions.bpl(29,1): Error BP5003: A postcondition might not hold on this return path.
+LambdaOldExpressions.bpl(23,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ LambdaOldExpressions.bpl(27,7): anon0
+
+Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/test2/LambdaPoly.bpl b/Test/test2/LambdaPoly.bpl
index 0fec0260..9a3fa16a 100644
--- a/Test/test2/LambdaPoly.bpl
+++ b/Test/test2/LambdaPoly.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
type set a = [a]bool;
function union<T>(a:set T, b:set T) : set T;
axiom (forall<T> a,b:set T :: union(a,b) == (lambda x:T :: a[x] || b[x]));
diff --git a/Test/test2/LambdaPoly.bpl.expect b/Test/test2/LambdaPoly.bpl.expect
new file mode 100644
index 00000000..9d080e36
--- /dev/null
+++ b/Test/test2/LambdaPoly.bpl.expect
@@ -0,0 +1,14 @@
+LambdaPoly.bpl(30,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LambdaPoly.bpl(26,5): anon0
+ LambdaPoly.bpl(29,5): anon4_Then
+LambdaPoly.bpl(33,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LambdaPoly.bpl(26,5): anon0
+ LambdaPoly.bpl(32,5): anon5_Then
+LambdaPoly.bpl(38,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LambdaPoly.bpl(26,5): anon0
+ LambdaPoly.bpl(36,5): anon5_Else
+
+Boogie program verifier finished with 1 verified, 3 errors
diff --git a/Test/test2/LoopInvAssume.bpl b/Test/test2/LoopInvAssume.bpl
index 1304e668..ecbcdc7c 100644
--- a/Test/test2/LoopInvAssume.bpl
+++ b/Test/test2/LoopInvAssume.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// Check that assumes in loop invariants are handled correctly
var x : int;
diff --git a/Test/test2/LoopInvAssume.bpl.expect b/Test/test2/LoopInvAssume.bpl.expect
new file mode 100644
index 00000000..6fda9cf0
--- /dev/null
+++ b/Test/test2/LoopInvAssume.bpl.expect
@@ -0,0 +1,6 @@
+LoopInvAssume.bpl(20,7): Error BP5001: This assertion might not hold.
+Execution trace:
+ LoopInvAssume.bpl(10,4): entry
+ LoopInvAssume.bpl(18,4): exit
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl
index 1e0fed76..c859afe4 100644
--- a/Test/test2/NeverPattern.bpl
+++ b/Test/test2/NeverPattern.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
function {:never_pattern true} f1(x:int) returns(int);
function {:never_pattern false} f2(x:int) returns(int);
function f3(x:int) returns(int);
diff --git a/Test/test2/NeverPattern.bpl.expect b/Test/test2/NeverPattern.bpl.expect
new file mode 100644
index 00000000..3ce334aa
--- /dev/null
+++ b/Test/test2/NeverPattern.bpl.expect
@@ -0,0 +1,11 @@
+NeverPattern.bpl(18,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NeverPattern.bpl(17,3): anon0
+NeverPattern.bpl(24,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NeverPattern.bpl(23,3): anon0
+NeverPattern.bpl(30,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NeverPattern.bpl(29,3): anon0
+
+Boogie program verifier finished with 2 verified, 3 errors
diff --git a/Test/test2/NullaryMaps.bpl b/Test/test2/NullaryMaps.bpl
index 1bc18c41..ed08ec93 100644
--- a/Test/test2/NullaryMaps.bpl
+++ b/Test/test2/NullaryMaps.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// aren't these cool!
var m: []int;
diff --git a/Test/test2/NullaryMaps.bpl.expect b/Test/test2/NullaryMaps.bpl.expect
new file mode 100644
index 00000000..bb48b1d5
--- /dev/null
+++ b/Test/test2/NullaryMaps.bpl.expect
@@ -0,0 +1,11 @@
+NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NullaryMaps.bpl(30,3): anon0
+NullaryMaps.bpl(32,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NullaryMaps.bpl(30,3): anon0
+NullaryMaps.bpl(38,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NullaryMaps.bpl(38,3): anon0
+
+Boogie program verifier finished with 2 verified, 3 errors
diff --git a/Test/test2/Old.bpl b/Test/test2/Old.bpl
index 00f798bc..99db9841 100644
--- a/Test/test2/Old.bpl
+++ b/Test/test2/Old.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var x: int;
var y: int;
diff --git a/Test/test2/Old.bpl.expect b/Test/test2/Old.bpl.expect
new file mode 100644
index 00000000..ca98d32b
--- /dev/null
+++ b/Test/test2/Old.bpl.expect
@@ -0,0 +1,6 @@
+Old.bpl(31,5): Error BP5003: A postcondition might not hold on this return path.
+Old.bpl(28,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Old.bpl(30,3): start
+
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/test2/OldIllegal.bpl b/Test/test2/OldIllegal.bpl
index 342c5b19..d2defb25 100644
--- a/Test/test2/OldIllegal.bpl
+++ b/Test/test2/OldIllegal.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// Test old appearing in illegal locations
var Global0: int;
diff --git a/Test/test2/OldIllegal.bpl.expect b/Test/test2/OldIllegal.bpl.expect
new file mode 100644
index 00000000..6c5f8013
--- /dev/null
+++ b/Test/test2/OldIllegal.bpl.expect
@@ -0,0 +1,3 @@
+OldIllegal.bpl(9,11): Error: old expressions allowed only in two-state contexts
+OldIllegal.bpl(16,23): Error: old expressions allowed only in two-state contexts
+2 name resolution errors detected in OldIllegal.bpl
diff --git a/Test/test2/Passification.bpl b/Test/test2/Passification.bpl
index e13d3e49..521a9d59 100644
--- a/Test/test2/Passification.bpl
+++ b/Test/test2/Passification.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// VC generation tests: passification
procedure good0(x: int) returns (y: int, z: int)
diff --git a/Test/test2/Passification.bpl.expect b/Test/test2/Passification.bpl.expect
new file mode 100644
index 00000000..65880ca4
--- /dev/null
+++ b/Test/test2/Passification.bpl.expect
@@ -0,0 +1,20 @@
+Passification.bpl(46,3): Error BP5003: A postcondition might not hold on this return path.
+Passification.bpl(38,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Passification.bpl(41,1): A
+Passification.bpl(118,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Passification.bpl(108,1): L0
+ Passification.bpl(113,1): L1
+ Passification.bpl(117,1): L2
+Passification.bpl(153,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Passification.bpl(146,1): L0
+ Passification.bpl(152,1): L2
+Passification.bpl(167,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Passification.bpl(160,1): L0
+ Passification.bpl(163,1): L1
+ Passification.bpl(166,1): L2
+
+Boogie program verifier finished with 7 verified, 4 errors
diff --git a/Test/test2/Quantifiers.bpl b/Test/test2/Quantifiers.bpl
index d368fe1f..e4a50c6b 100644
--- a/Test/test2/Quantifiers.bpl
+++ b/Test/test2/Quantifiers.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
// ----------------------------------------------------------------------- single trigger
function f(int, int) returns (int);
diff --git a/Test/test2/Quantifiers.bpl.expect b/Test/test2/Quantifiers.bpl.expect
new file mode 100644
index 00000000..59c3d403
--- /dev/null
+++ b/Test/test2/Quantifiers.bpl.expect
@@ -0,0 +1,20 @@
+Quantifiers.bpl(22,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Quantifiers.bpl(21,3): start
+Quantifiers.bpl(45,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Quantifiers.bpl(44,3): start
+Quantifiers.bpl(67,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Quantifiers.bpl(66,3): start
+Quantifiers.bpl(75,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Quantifiers.bpl(73,3): start
+Quantifiers.bpl(127,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Quantifiers.bpl(126,3): start
+Quantifiers.bpl(152,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Quantifiers.bpl(151,3): start
+
+Boogie program verifier finished with 8 verified, 6 errors
diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl
index ed40787e..16d5bc82 100644
--- a/Test/test2/SelectiveChecking.bpl
+++ b/Test/test2/SelectiveChecking.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure {:selective_checking} foo()
{
var x, y, z : int;
diff --git a/Test/test2/SelectiveChecking.bpl.expect b/Test/test2/SelectiveChecking.bpl.expect
new file mode 100644
index 00000000..8b5d33b0
--- /dev/null
+++ b/Test/test2/SelectiveChecking.bpl.expect
@@ -0,0 +1,16 @@
+SelectiveChecking.bpl(19,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(17,3): anon0
+SelectiveChecking.bpl(32,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(26,3): anon0
+ SelectiveChecking.bpl(29,5): anon3_Then
+ SelectiveChecking.bpl(32,3): anon2
+SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(39,3): anon0
+SelectiveChecking.bpl(41,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(39,3): anon0
+
+Boogie program verifier finished with 1 verified, 4 errors
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl
index d5ce8cf4..7a4ad46d 100644
--- a/Test/test2/Structured.bpl
+++ b/Test/test2/Structured.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
const K: int;
diff --git a/Test/test2/Structured.bpl.expect b/Test/test2/Structured.bpl.expect
new file mode 100644
index 00000000..cd8a1567
--- /dev/null
+++ b/Test/test2/Structured.bpl.expect
@@ -0,0 +1,20 @@
+Structured.bpl(254,14): Error BP5003: A postcondition might not hold on this return path.
+Structured.bpl(245,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Structured.bpl(246,5): anon0
+ Structured.bpl(248,5): anon6_LoopBody
+ Structured.bpl(249,7): anon7_LoopBody
+ Structured.bpl(250,11): anon8_Then
+ Structured.bpl(254,14): anon9_Then
+Structured.bpl(305,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Structured.bpl(301,5): anon0
+ Structured.bpl(302,3): anon3_Else
+ Structured.bpl(305,3): anon2
+Structured.bpl(313,7): Error BP5001: This assertion might not hold.
+Execution trace:
+ Structured.bpl(310,3): anon0
+ Structured.bpl(310,3): anon1_Then
+ Structured.bpl(311,5): A
+
+Boogie program verifier finished with 16 verified, 3 errors
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl
index c874a1c1..51b6655f 100644
--- a/Test/test2/Timeouts0.bpl
+++ b/Test/test2/Timeouts0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -timeLimit:4 %s > %t
+// RUN: %diff %s.expect %t
procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int)
requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
requires 0 < len;
diff --git a/Test/test2/Timeouts0.bpl.expect b/Test/test2/Timeouts0.bpl.expect
new file mode 100644
index 00000000..6c95b9bd
--- /dev/null
+++ b/Test/test2/Timeouts0.bpl.expect
@@ -0,0 +1,47 @@
+Timeouts0.bpl(21,5): Error BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(6,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(10,7): anon0
+ Timeouts0.bpl(12,5): anon4_LoopHead
+ Timeouts0.bpl(12,5): anon4_LoopDone
+ Timeouts0.bpl(21,5): anon5_LoopHead
+ Timeouts0.bpl(21,5): anon5_LoopDone
+Timeouts0.bpl(23,7): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(10,7): anon0
+ Timeouts0.bpl(12,5): anon4_LoopHead
+ Timeouts0.bpl(12,5): anon4_LoopDone
+ Timeouts0.bpl(21,5): anon5_LoopHead
+ Timeouts0.bpl(25,11): anon5_LoopBody
+Timeouts0.bpl(50,5): Error BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(33,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(39,7): anon0
+ Timeouts0.bpl(41,5): anon4_LoopHead
+ Timeouts0.bpl(41,5): anon4_LoopDone
+ Timeouts0.bpl(50,5): anon5_LoopHead
+ Timeouts0.bpl(50,5): anon5_LoopDone
+Timeouts0.bpl(52,7): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(39,7): anon0
+ Timeouts0.bpl(41,5): anon4_LoopHead
+ Timeouts0.bpl(41,5): anon4_LoopDone
+ Timeouts0.bpl(50,5): anon5_LoopHead
+ Timeouts0.bpl(54,11): anon5_LoopBody
+Timeouts0.bpl(79,5): Error BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(62,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(68,7): anon0
+ Timeouts0.bpl(70,5): anon4_LoopHead
+ Timeouts0.bpl(70,5): anon4_LoopDone
+ Timeouts0.bpl(79,5): anon5_LoopHead
+ Timeouts0.bpl(79,5): anon5_LoopDone
+Timeouts0.bpl(81,7): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(68,7): anon0
+ Timeouts0.bpl(70,5): anon4_LoopHead
+ Timeouts0.bpl(70,5): anon4_LoopDone
+ Timeouts0.bpl(79,5): anon5_LoopHead
+ Timeouts0.bpl(83,11): anon5_LoopBody
+
+Boogie program verifier finished with 0 verified, 6 errors
diff --git a/Test/test2/TypeEncodingM.bpl b/Test/test2/TypeEncodingM.bpl
index 01c95f7a..8a1bc803 100644
--- a/Test/test2/TypeEncodingM.bpl
+++ b/Test/test2/TypeEncodingM.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m %s > %t
+// RUN: %diff %s.expect %t
type TT;
procedure A()
diff --git a/Test/test2/TypeEncodingM.bpl.expect b/Test/test2/TypeEncodingM.bpl.expect
new file mode 100644
index 00000000..ea29f1d0
--- /dev/null
+++ b/Test/test2/TypeEncodingM.bpl.expect
@@ -0,0 +1,5 @@
+TypeEncodingM.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ TypeEncodingM.bpl(13,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test2/UpdateExpr.bpl b/Test/test2/UpdateExpr.bpl
index 8f950073..d89c4715 100644
--- a/Test/test2/UpdateExpr.bpl
+++ b/Test/test2/UpdateExpr.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
const a: [int]bool;
diff --git a/Test/test2/UpdateExpr.bpl.expect b/Test/test2/UpdateExpr.bpl.expect
new file mode 100644
index 00000000..30dc8529
--- /dev/null
+++ b/Test/test2/UpdateExpr.bpl.expect
@@ -0,0 +1,17 @@
+UpdateExpr.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ UpdateExpr.bpl(16,3): anon0
+UpdateExpr.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ UpdateExpr.bpl(21,3): anon0
+UpdateExpr.bpl(34,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ UpdateExpr.bpl(34,3): anon0
+UpdateExpr.bpl(40,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ UpdateExpr.bpl(40,3): anon0
+UpdateExpr.bpl(54,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ UpdateExpr.bpl(53,5): anon0
+
+Boogie program verifier finished with 5 verified, 5 errors
diff --git a/Test/test2/Where.bpl b/Test/test2/Where.bpl
index 96ffcf04..031398ed 100644
--- a/Test/test2/Where.bpl
+++ b/Test/test2/Where.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
procedure P0()
{
var x: int where 0 <= x;
diff --git a/Test/test2/Where.bpl.expect b/Test/test2/Where.bpl.expect
new file mode 100644
index 00000000..a0399042
--- /dev/null
+++ b/Test/test2/Where.bpl.expect
@@ -0,0 +1,37 @@
+Where.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(8,3): anon0
+Where.bpl(24,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(18,5): anon0
+Where.bpl(34,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(32,3): anon0
+Where.bpl(46,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(42,5): anon0
+Where.bpl(59,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(54,3): anon0
+Where.bpl(113,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(104,5): anon0
+ Where.bpl(106,3): anon3_LoopHead
+ Where.bpl(106,3): anon3_LoopDone
+Where.bpl(130,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(123,5): anon0
+ Where.bpl(124,3): anon3_LoopHead
+ Where.bpl(124,3): anon3_LoopDone
+Where.bpl(147,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(140,5): anon0
+ Where.bpl(141,3): anon3_LoopHead
+ Where.bpl(141,3): anon3_LoopDone
+Where.bpl(164,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Where.bpl(157,5): anon0
+ Where.bpl(158,3): anon3_LoopHead
+ Where.bpl(158,3): anon3_LoopDone
+
+Boogie program verifier finished with 2 verified, 9 errors
diff --git a/Test/test2/sk_hack.bpl b/Test/test2/sk_hack.bpl
index df942317..1d902a74 100644
--- a/Test/test2/sk_hack.bpl
+++ b/Test/test2/sk_hack.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
function in_set(int) returns(bool);
function next(int) returns(int);
function f(int) returns(bool);
diff --git a/Test/test2/sk_hack.bpl.expect b/Test/test2/sk_hack.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/test2/sk_hack.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl
index 6aee18ea..e451cc3e 100644
--- a/Test/test2/strings-no-where.bpl
+++ b/Test/test2/strings-no-where.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
type elements;
diff --git a/Test/test2/strings-no-where.bpl.expect b/Test/test2/strings-no-where.bpl.expect
new file mode 100644
index 00000000..df9c7d8b
--- /dev/null
+++ b/Test/test2/strings-no-where.bpl.expect
@@ -0,0 +1,19 @@
+strings-no-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)
+strings-no-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-no-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)
+strings-no-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-no-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-no-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)
+strings-no-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-no-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator ==
+strings-no-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any)
+strings-no-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator ==
+18 type checking errors detected in strings-no-where.bpl
diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl
index f196899f..86804051 100644
--- a/Test/test2/strings-where.bpl
+++ b/Test/test2/strings-where.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
type elements;
diff --git a/Test/test2/strings-where.bpl.expect b/Test/test2/strings-where.bpl.expect
new file mode 100644
index 00000000..aa7fe2bb
--- /dev/null
+++ b/Test/test2/strings-where.bpl.expect
@@ -0,0 +1,19 @@
+strings-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any)
+strings-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any)
+strings-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any)
+strings-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any)
+strings-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any)
+strings-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator ==
+strings-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any)
+strings-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator ==
+18 type checking errors detected in strings-where.bpl