diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-10 15:35:07 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-10 15:35:07 +0100 |
| commit | 88a5ed2e9a79118fa45f195360aa10597a182fec (patch) | |
| tree | fd3fd1ef1a6956616e3a42dc55adf0aaa394ee5c /Test/test2 | |
| parent | 631da48e5bffbdd66ac6f076a8beb120385addfa (diff) | |
Unbreak the tests in test2 for batch file testing infrastructure
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5d446e64..9403e6a9 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -81,14 +81,14 @@ 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(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.
+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(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.
+ 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(125,3): start
+ Arrays.bpl(127,3): start
Boogie program verifier finished with 8 verified, 2 errors
@@ -362,12 +362,12 @@ Execution trace: Boogie program verifier finished with 2 verified, 2 errors
-------------------- Lambda.bpl --------------------
-Lambda.bpl(39,3): Error BP5001: This assertion might not hold.
+Lambda.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
-Lambda.bpl(40,3): Error BP5001: This assertion might not hold.
+ Lambda.bpl(40,5): anon0
+Lambda.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
+ Lambda.bpl(40,5): anon0
Boogie program verifier finished with 6 verified, 2 errors
@@ -447,24 +447,24 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
-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.
+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(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.
+ 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(125,3): start
+ Arrays.bpl(127,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Lambda.bpl /typeEncoding:m --------------------
-Lambda.bpl(39,3): Error BP5001: This assertion might not hold.
+Lambda.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
-Lambda.bpl(40,3): Error BP5001: This assertion might not hold.
+ Lambda.bpl(40,5): anon0
+Lambda.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
+ Lambda.bpl(40,5): anon0
Boogie program verifier finished with 6 verified, 2 errors
|