Skip to content

Commit 757534d

Browse files
committed
Fix indexing in expected test output
1 parent eef75d5 commit 757534d

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

Test/coverage/verificationCoverage.bpl.expect-trace

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ Proof dependencies:
1212

1313
Verifying sum ...
1414
Proof dependencies:
15+
id_l127_c3_assume_0
1516
id_l127_c3_assume_1
16-
id_l127_c3_assume_2
1717
invariant sinv_not_1 established
1818
invariant sinv_not_1 maintained
1919
invariant sinv1 assumed in body
@@ -80,7 +80,7 @@ verificationCoverage.bpl(203,2): Warning: Proved vacuously
8080

8181
Verifying usesSomeInteger ...
8282
Proof dependencies:
83-
id_l216_c3_ensures_3
83+
id_l216_c3_ensures_2
8484
someInteger_value_axiom
8585
Proof dependencies of whole program:
8686
a_gt_10
@@ -99,9 +99,9 @@ Proof dependencies of whole program:
9999
ensures clause tee0 from call call2
100100
ensures clause tee1 from call call2
101101
false_req
102+
id_l127_c3_assume_0
102103
id_l127_c3_assume_1
103-
id_l127_c3_assume_2
104-
id_l216_c3_ensures_3
104+
id_l216_c3_ensures_2
105105
invariant sinv_not_1 established
106106
invariant sinv_not_1 maintained
107107
invariant sinv1 assumed in body

0 commit comments

Comments
 (0)