diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:45:05 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:45:05 +0100 |
| commit | 73a1c73067c3664187d2cc98e5b6abc04b6691c2 (patch) | |
| tree | c04e2ac512553b3ea4d07cac735cbee166c0e3e4 /Test/stratifiedinline | |
| parent | 9fe2b84adc90a4c58b16188c4c3b947d7d564039 (diff) | |
Enabled the "Stratified inlining benchmarks" lit tests.
The following tests will probably fail for newer versions
of Z3 (e.g. 4.3)
stratifiedinline/bar10.bpl
stratifiedinline/bar7.bpl
stratifiedinline/bar8.bpl
stratifiedinline/bar9.bpl
Diffstat (limited to 'Test/stratifiedinline')
27 files changed, 750 insertions, 231 deletions
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index 27d2be6b..2a3d7605 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,14 +1,14 @@ ----- Running regression test bar1.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar1.bpl(22,3): anon0
+ bar1.bpl(24,3): anon0
Inlined call to procedure foo begins
- bar1.bpl(13,5): anon0
+ bar1.bpl(15,5): anon0
Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
+ bar1.bpl(9,5): anon0
Inlined call to procedure bar ends
Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
+ bar1.bpl(9,5): anon0
Inlined call to procedure bar ends
Inlined call to procedure foo ends
@@ -17,14 +17,14 @@ Boogie program verifier finished with 0 verified, 1 error ----- Running regression test bar2.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar2.bpl(18,3): anon0
+ bar2.bpl(20,3): anon0
Inlined call to procedure foo begins
- bar2.bpl(4,3): anon0
- bar2.bpl(5,7): anon3_Then
+ bar2.bpl(6,3): anon0
+ bar2.bpl(7,7): anon3_Then
Inlined call to procedure foo ends
Inlined call to procedure foo begins
- bar2.bpl(4,3): anon0
- bar2.bpl(8,7): anon3_Else
+ bar2.bpl(6,3): anon0
+ bar2.bpl(10,7): anon3_Else
Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
@@ -32,22 +32,22 @@ Boogie program verifier finished with 0 verified, 1 error ----- Running regression test bar3.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar3.bpl(35,3): anon0
+ bar3.bpl(37,3): anon0
Inlined call to procedure foo begins
- bar3.bpl(18,3): anon0
- bar3.bpl(19,7): anon3_Then
+ bar3.bpl(20,3): anon0
+ bar3.bpl(21,7): anon3_Then
Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
+ bar3.bpl(9,3): anon0
+ bar3.bpl(10,7): anon3_Then
Inlined call to procedure bar ends
Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
+ bar3.bpl(9,3): anon0
+ bar3.bpl(10,7): anon3_Then
Inlined call to procedure bar ends
Inlined call to procedure foo ends
Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(10,7): anon3_Else
+ bar3.bpl(9,3): anon0
+ bar3.bpl(12,7): anon3_Else
Inlined call to procedure bar ends
Boogie program verifier finished with 0 verified, 1 error
@@ -63,71 +63,71 @@ Boogie program verifier finished with 1 verified, 0 errors ----- Running regression test bar7.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar7.bpl(35,5): anon0
- bar7.bpl(37,5): anon4_Then
+ bar7.bpl(37,5): anon0
+ bar7.bpl(39,5): anon4_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(8,9): anon2_Then
+ bar7.bpl(9,3): anon0
+ bar7.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar7.bpl(7,3): anon0
- bar7.bpl(7,3): anon2_Else
+ bar7.bpl(9,3): anon0
+ bar7.bpl(9,3): anon2_Else
Inlined call to procedure foo ends
Inlined call to procedure foo ends
Inlined call to procedure foo ends
@@ -149,78 +149,78 @@ Execution trace: Inlined call to procedure foo ends
Inlined call to procedure foo ends
Inlined call to procedure foo ends
- bar7.bpl(42,3): anon3
+ bar7.bpl(44,3): anon3
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar8.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar8.bpl(34,5): anon0
- bar8.bpl(36,5): anon4_Then
+ bar8.bpl(36,5): anon0
+ bar8.bpl(38,5): anon4_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(8,9): anon2_Then
+ bar8.bpl(9,3): anon0
+ bar8.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar8.bpl(7,3): anon0
- bar8.bpl(7,3): anon2_Else
+ bar8.bpl(9,3): anon0
+ bar8.bpl(9,3): anon2_Else
Inlined call to procedure foo ends
Inlined call to procedure foo ends
Inlined call to procedure foo ends
@@ -242,78 +242,78 @@ Execution trace: Inlined call to procedure foo ends
Inlined call to procedure foo ends
Inlined call to procedure foo ends
- bar8.bpl(41,3): anon3
+ bar8.bpl(43,3): anon3
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar9.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar9.bpl(35,5): anon0
- bar9.bpl(41,5): anon4_Else
+ bar9.bpl(37,5): anon0
+ bar9.bpl(43,5): anon4_Else
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(18,7): anon2_Then
+ bar9.bpl(18,3): anon0
+ bar9.bpl(20,7): anon2_Then
Inlined call to procedure bar1 begins
- bar9.bpl(16,3): anon0
- bar9.bpl(16,3): anon2_Else
+ bar9.bpl(18,3): anon0
+ bar9.bpl(18,3): anon2_Else
Inlined call to procedure bar1 ends
Inlined call to procedure bar1 ends
Inlined call to procedure bar1 ends
@@ -336,38 +336,38 @@ Execution trace: Inlined call to procedure bar1 ends
Inlined call to procedure bar1 ends
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(27,7): anon2_Then
+ bar9.bpl(28,3): anon0
+ bar9.bpl(29,7): anon2_Then
Inlined call to procedure bar2 begins
- bar9.bpl(26,3): anon0
- bar9.bpl(26,3): anon2_Else
+ bar9.bpl(28,3): anon0
+ bar9.bpl(28,3): anon2_Else
Inlined call to procedure bar2 ends
Inlined call to procedure bar2 ends
Inlined call to procedure bar2 ends
@@ -379,85 +379,85 @@ Execution trace: Inlined call to procedure bar2 ends
Inlined call to procedure bar2 ends
Inlined call to procedure bar2 ends
- bar9.bpl(44,3): anon3
+ bar9.bpl(46,3): anon3
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar10.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar10.bpl(35,5): anon0
+ bar10.bpl(37,5): anon0
Inlined call to procedure bar1 begins
- bar10.bpl(16,3): anon0
- bar10.bpl(16,3): anon2_Else
+ bar10.bpl(18,3): anon0
+ bar10.bpl(18,3): anon2_Else
Inlined call to procedure bar1 ends
Inlined call to procedure bar2 begins
- bar10.bpl(26,3): anon0
- bar10.bpl(26,3): anon2_Else
+ bar10.bpl(28,3): anon0
+ bar10.bpl(28,3): anon2_Else
Inlined call to procedure bar2 ends
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(8,9): anon2_Then
+ bar10.bpl(9,3): anon0
+ bar10.bpl(10,9): anon2_Then
Inlined call to procedure foo begins
- bar10.bpl(7,3): anon0
- bar10.bpl(7,3): anon2_Else
+ bar10.bpl(9,3): anon0
+ bar10.bpl(9,3): anon2_Else
Inlined call to procedure foo ends
Inlined call to procedure foo ends
Inlined call to procedure foo ends
@@ -485,16 +485,16 @@ Boogie program verifier finished with 0 verified, 1 error ----- Running regression test bar11.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar11.bpl(26,3): anon0
+ bar11.bpl(28,3): anon0
Inlined call to procedure foo begins
- bar11.bpl(15,3): anon0
+ bar11.bpl(17,3): anon0
value = 0
Inlined call to procedure bar begins
- bar11.bpl(8,5): anon0
+ bar11.bpl(10,5): anon0
value = 1
Inlined call to procedure bar ends
Inlined call to procedure bar begins
- bar11.bpl(8,5): anon0
+ bar11.bpl(10,5): anon0
value = 2
Inlined call to procedure bar ends
value = 2
@@ -505,7 +505,7 @@ Boogie program verifier finished with 0 verified, 1 error ----- Running regression test bar12.bpl
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar12.bpl(6,4): anon0
+ bar12.bpl(8,4): anon0
Boogie program verifier finished with 0 verified, 1 error
-----
diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl index bd210f70..48cef01f 100644 --- a/Test/stratifiedinline/bar1.bpl +++ b/Test/stratifiedinline/bar1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
var x: int;
var y: int;
diff --git a/Test/stratifiedinline/bar1.bpl.expect b/Test/stratifiedinline/bar1.bpl.expect new file mode 100644 index 00000000..7dd67011 --- /dev/null +++ b/Test/stratifiedinline/bar1.bpl.expect @@ -0,0 +1,14 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar1.bpl(24,3): anon0 + Inlined call to procedure foo begins + bar1.bpl(15,5): anon0 + Inlined call to procedure bar begins + bar1.bpl(9,5): anon0 + Inlined call to procedure bar ends + Inlined call to procedure bar begins + bar1.bpl(9,5): anon0 + Inlined call to procedure bar ends + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl index ab1e4748..3ec0f72f 100644 --- a/Test/stratifiedinline/bar10.bpl +++ b/Test/stratifiedinline/bar10.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
+// RUN: %diff %s.expect %t
var i: int;
var m: int;
@@ -38,4 +40,4 @@ modifies i; i := 0;
call foo();
assume !(i < 10);
-}
\ No newline at end of file +}
diff --git a/Test/stratifiedinline/bar10.bpl.expect b/Test/stratifiedinline/bar10.bpl.expect new file mode 100644 index 00000000..44eb9ef4 --- /dev/null +++ b/Test/stratifiedinline/bar10.bpl.expect @@ -0,0 +1,97 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar10.bpl(37,5): anon0 + Inlined call to procedure bar1 begins + bar10.bpl(18,3): anon0 + bar10.bpl(18,3): anon2_Else + Inlined call to procedure bar1 ends + Inlined call to procedure bar2 begins + bar10.bpl(28,3): anon0 + bar10.bpl(28,3): anon2_Else + Inlined call to procedure bar2 ends + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(9,3): anon0 + bar10.bpl(9,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl index 67e21ba6..4d1fffa0 100644 --- a/Test/stratifiedinline/bar11.bpl +++ b/Test/stratifiedinline/bar11.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
var x: int;
var y: int;
procedure boogie_si_record_int(x:int);
diff --git a/Test/stratifiedinline/bar11.bpl.expect b/Test/stratifiedinline/bar11.bpl.expect new file mode 100644 index 00000000..bd5dbbf4 --- /dev/null +++ b/Test/stratifiedinline/bar11.bpl.expect @@ -0,0 +1,18 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar11.bpl(28,3): anon0 + Inlined call to procedure foo begins + bar11.bpl(17,3): anon0 + value = 0 + Inlined call to procedure bar begins + bar11.bpl(10,5): anon0 + value = 1 + Inlined call to procedure bar ends + Inlined call to procedure bar begins + bar11.bpl(10,5): anon0 + value = 2 + Inlined call to procedure bar ends + value = 2 + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar12.bpl b/Test/stratifiedinline/bar12.bpl index 863f9dc0..a129a02b 100644 --- a/Test/stratifiedinline/bar12.bpl +++ b/Test/stratifiedinline/bar12.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
function {:inline} f(a:bool) : bool { true }
procedure {:entrypoint} main()
diff --git a/Test/stratifiedinline/bar12.bpl.expect b/Test/stratifiedinline/bar12.bpl.expect new file mode 100644 index 00000000..ab9eae00 --- /dev/null +++ b/Test/stratifiedinline/bar12.bpl.expect @@ -0,0 +1,5 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar12.bpl(8,4): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar13.bpl b/Test/stratifiedinline/bar13.bpl index bdeaaa51..fc4f35b0 100644 --- a/Test/stratifiedinline/bar13.bpl +++ b/Test/stratifiedinline/bar13.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
var alloc: int;
var assertsPassed: bool;
procedure boogie_si_record_li2bpl_int(x: int);
diff --git a/Test/stratifiedinline/bar13.bpl.expect b/Test/stratifiedinline/bar13.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/stratifiedinline/bar13.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl index 6c383591..2f680760 100644 --- a/Test/stratifiedinline/bar2.bpl +++ b/Test/stratifiedinline/bar2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
procedure foo() returns (x: bool)
{
var b: bool;
diff --git a/Test/stratifiedinline/bar2.bpl.expect b/Test/stratifiedinline/bar2.bpl.expect new file mode 100644 index 00000000..e6e3c699 --- /dev/null +++ b/Test/stratifiedinline/bar2.bpl.expect @@ -0,0 +1,13 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar2.bpl(20,3): anon0 + Inlined call to procedure foo begins + bar2.bpl(6,3): anon0 + bar2.bpl(7,7): anon3_Then + Inlined call to procedure foo ends + Inlined call to procedure foo begins + bar2.bpl(6,3): anon0 + bar2.bpl(10,7): anon3_Else + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl index a1f0bea3..60fc8989 100644 --- a/Test/stratifiedinline/bar3.bpl +++ b/Test/stratifiedinline/bar3.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
var y: int;
var x: int;
diff --git a/Test/stratifiedinline/bar3.bpl.expect b/Test/stratifiedinline/bar3.bpl.expect new file mode 100644 index 00000000..a00bd218 --- /dev/null +++ b/Test/stratifiedinline/bar3.bpl.expect @@ -0,0 +1,21 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar3.bpl(37,3): anon0 + Inlined call to procedure foo begins + bar3.bpl(20,3): anon0 + bar3.bpl(21,7): anon3_Then + Inlined call to procedure bar begins + bar3.bpl(9,3): anon0 + bar3.bpl(10,7): anon3_Then + Inlined call to procedure bar ends + Inlined call to procedure bar begins + bar3.bpl(9,3): anon0 + bar3.bpl(10,7): anon3_Then + Inlined call to procedure bar ends + Inlined call to procedure foo ends + Inlined call to procedure bar begins + bar3.bpl(9,3): anon0 + bar3.bpl(12,7): anon3_Else + Inlined call to procedure bar ends + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl index 4b3a6ee2..8e439288 100644 --- a/Test/stratifiedinline/bar4.bpl +++ b/Test/stratifiedinline/bar4.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
var y: int;
var x: int;
diff --git a/Test/stratifiedinline/bar4.bpl.expect b/Test/stratifiedinline/bar4.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/stratifiedinline/bar4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl index dd528f6f..33a06462 100644 --- a/Test/stratifiedinline/bar6.bpl +++ b/Test/stratifiedinline/bar6.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
var M: [int]int;
procedure bar(y: int) returns (b: bool)
diff --git a/Test/stratifiedinline/bar6.bpl.expect b/Test/stratifiedinline/bar6.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/stratifiedinline/bar6.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index 41cf612e..531f9f43 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
+// RUN: %diff %s.expect %t
var i: int;
var m: int;
@@ -40,4 +42,4 @@ modifies i; call bar2(0);
}
assume !(i < 10);
-}
\ No newline at end of file +}
diff --git a/Test/stratifiedinline/bar7.bpl.expect b/Test/stratifiedinline/bar7.bpl.expect new file mode 100644 index 00000000..c56460bd --- /dev/null +++ b/Test/stratifiedinline/bar7.bpl.expect @@ -0,0 +1,91 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar7.bpl(37,5): anon0 + bar7.bpl(39,5): anon4_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(9,3): anon0 + bar7.bpl(9,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + bar7.bpl(44,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index 356645e6..a1c63b72 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
+// RUN: %diff %s.expect %t
var i: int;
var m: int;
@@ -39,4 +41,4 @@ modifies i; call bar2(0);
}
assume !(i < 10);
-}
\ No newline at end of file +}
diff --git a/Test/stratifiedinline/bar8.bpl.expect b/Test/stratifiedinline/bar8.bpl.expect new file mode 100644 index 00000000..44612154 --- /dev/null +++ b/Test/stratifiedinline/bar8.bpl.expect @@ -0,0 +1,91 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar8.bpl(36,5): anon0 + bar8.bpl(38,5): anon4_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(10,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(9,3): anon0 + bar8.bpl(9,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + bar8.bpl(43,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl index d1eacb18..da89dbf3 100644 --- a/Test/stratifiedinline/bar9.bpl +++ b/Test/stratifiedinline/bar9.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i -nonUniformUnfolding %s > %t
+// RUN: %diff %s.expect %t
var i: int;
var m: int;
@@ -42,4 +44,4 @@ modifies i; call bar2(0);
}
assume !(i < 10);
-}
\ No newline at end of file +}
diff --git a/Test/stratifiedinline/bar9.bpl.expect b/Test/stratifiedinline/bar9.bpl.expect new file mode 100644 index 00000000..ff58339a --- /dev/null +++ b/Test/stratifiedinline/bar9.bpl.expect @@ -0,0 +1,135 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + bar9.bpl(37,5): anon0 + bar9.bpl(43,5): anon4_Else + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(20,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(18,3): anon0 + bar9.bpl(18,3): anon2_Else + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(29,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(28,3): anon0 + bar9.bpl(28,3): anon2_Else + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + bar9.bpl(46,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/stratifiedinline/large.bpl b/Test/stratifiedinline/large.bpl index 3b7196bb..44e4e7fc 100644 --- a/Test/stratifiedinline/large.bpl +++ b/Test/stratifiedinline/large.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -vc:i %s > %t
+// RUN: %diff %s.expect %t
procedure proc63() returns (nVar5796: int, nVar5797: bool);
modifies nVar2, nVar1, nVar3, nVar4, nVar5, nVar6, nVar7, nVar8, nVar9, nVar10, nVar11, nVar12, nVar13, nVar14, nVar15, nVar16, nVar17, nVar18, nVar19, nVar20, nVar21, nVar22, nVar23, nVar24, nVar25, nVar26, nVar27, nVar28, nVar29, nVar30, nVar31, nVar32, nVar33, nVar34, nVar35, nVar36, nVar37, nVar38, nVar39, nVar40, nVar41, nVar42, nVar43, nVar44, nVar45, nVar46, nVar47, nVar48, nVar49, nVar50, nVar51, nVar52, nVar53, nVar54, nVar55, nVar56, nVar57, nVar58, nVar59, nVar60, nVar61, nVar62, nVar63, nVar64, nVar65, nVar66, nVar67, nVar68, nVar69, nVar70, nVar71, nVar72, nVar73, nVar74, nVar75, nVar76, nVar77, nVar78, nVar79, nVar80, nVar81, nVar82, nVar83, nVar84, nVar85, nVar86, nVar87, nVar88, nVar89, nVar90, nVar91, nVar92, nVar93, nVar94, nVar95, nVar96, nVar97, nVar98, nVar99, nVar100, nVar101, nVar102, nVar103, nVar104, nVar105, nVar106, nVar107, nVar108, nVar109, nVar110, nVar111, nVar112, nVar113, nVar114, nVar115, nVar116, nVar117, nVar118, nVar119, nVar120, nVar121, nVar122, nVar123, nVar124, nVar125, nVar126, nVar127, nVar128, nVar129, nVar130, nVar131, nVar132, nVar133, nVar134, nVar135, nVar136, nVar137, nVar138, nVar139, nVar140, nVar141, nVar142, nVar143, nVar144, nVar145, nVar146, nVar147, nVar148, nVar149, nVar150, nVar151, nVar152, nVar153, nVar154, nVar155, nVar156, nVar157, nVar158, nVar159, nVar160, nVar161, nVar162, nVar163, nVar164, nVar165, nVar166, nVar167, nVar168, nVar169, nVar170, nVar171, nVar172, nVar173, nVar174, nVar175, nVar176, nVar177, nVar178, nVar179, nVar180, nVar181, nVar182, nVar183, nVar184, nVar185, nVar186, nVar187, nVar188, nVar189, nVar190, nVar191, nVar192, nVar193, nVar194, nVar195, nVar196, nVar197, nVar198, nVar199, nVar200, nVar201, nVar202, nVar203, nVar204, nVar205, nVar206, nVar207, nVar208, nVar209, nVar210, nVar211, nVar212, nVar213, nVar214, nVar215, nVar216, nVar217, nVar218, nVar219, nVar220, nVar221, nVar222, nVar223, nVar224, nVar225, nVar226, nVar227, nVar228, nVar229, nVar230, nVar231, nVar232, nVar233, nVar234, nVar235, nVar236, nVar237, nVar238, nVar239, nVar240, nVar241, nVar242, nVar243, nVar244, nVar245, nVar246, nVar247, nVar248, nVar249, nVar250, nVar251, nVar252, nVar253, nVar254, nVar255, nVar256, nVar257, nVar258, nVar259, nVar260, nVar261, nVar262, nVar263, nVar264, nVar265, nVar266, nVar267, nVar268, nVar269, nVar270, nVar271, nVar272, nVar273, nVar274, nVar275, nVar276, nVar277, nVar278, nVar279, nVar281, nVar282, nVar283, nVar284, nVar285, nVar286, nVar287, nVar288, nVar289, nVar290, nVar291, nVar292, nVar293, nVar294, nVar295, nVar296, nVar297, nVar298, nVar299, nVar300, nVar301, nVar302, nVar303, nVar304, nVar305, nVar306, nVar307, nVar308, nVar309, nVar310, nVar311, nVar312, nVar313, nVar314, nVar315, nVar316, nVar317, nVar318, nVar319, nVar320, nVar321, nVar322, nVar323, nVar324, nVar325, nVar326, nVar327, nVar328, nVar329, nVar330, nVar331, nVar332, nVar333, nVar334, nVar335, nVar336, nVar337, nVar338, nVar339, nVar340, nVar341, nVar342, nVar343, nVar344, nVar345, nVar346, nVar348, nVar349, nVar350, nVar351, nVar352, nVar353, nVar354, nVar355, nVar356, nVar357, nVar358, nVar359, nVar360, nVar361, nVar362, nVar363, nVar364, nVar365, nVar366, nVar367, nVar368, nVar369, nVar370, nVar371, nVar372, nVar373, nVar374, nVar375, nVar376, nVar377, nVar378, nVar379, nVar380, nVar381, nVar382, nVar383, nVar384, nVar385, nVar386, nVar387, nVar388, nVar389, nVar390, nVar391, nVar392, nVar393, nVar394, nVar395, nVar396, nVar397, nVar398, nVar400, nVar401, nVar402, nVar403, nVar404, nVar405, nVar406, nVar407, nVar408, nVar409, nVar410, nVar411, nVar412, nVar413, nVar414, nVar415, nVar416, nVar417, nVar418, nVar419, nVar420, nVar421, nVar422, nVar423, nVar424, nVar425, nVar426, nVar427, nVar428, nVar429, nVar430, nVar431, nVar432, nVar433, nVar434, nVar435, nVar436, nVar437, nVar438, nVar439, nVar440, nVar441, nVar442, nVar443, nVar444, nVar445, nVar446, nVar447, nVar448, nVar449, nVar450, nVar451, nVar452, nVar453, nVar454, nVar455, nVar456, nVar457, nVar458, nVar459, nVar460, nVar461, nVar462, nVar463, nVar464, nVar465, nVar466, nVar467, nVar468, nVar469, nVar470, nVar471, nVar472, nVar473, nVar474, nVar475, nVar476, nVar477, nVar478, nVar479, nVar480, nVar481, nVar482, nVar483, nVar484, nVar485, nVar486, nVar487, nVar488, nVar489, nVar490, nVar491, nVar492, nVar493, nVar494, nVar495, nVar496, nVar497, nVar498, nVar499, nVar500, nVar501, nVar502, nVar503, nVar504, nVar505, nVar506, nVar507, nVar508, nVar509, nVar510, nVar511, nVar512, nVar513, nVar514, nVar515, nVar516, nVar517, nVar518, nVar519, nVar520, nVar521, nVar522, nVar523, nVar524, nVar525, nVar526, nVar527, nVar528, nVar529, nVar530, nVar531, nVar532, nVar533, nVar534, nVar535, nVar536, nVar537, nVar538, nVar539, nVar540, nVar541, nVar542, nVar543, nVar544, nVar545, nVar546, nVar547, nVar548, nVar549, nVar550, nVar551, nVar552, nVar553, nVar554, nVar555, nVar556, nVar557, nVar558, nVar559, nVar560, nVar561, nVar562, nVar563, nVar564, nVar565, nVar566, nVar567, nVar568, nVar569, nVar570, nVar571, nVar572, nVar573, nVar574, nVar575, nVar576, nVar577, nVar578, nVar579, nVar580, nVar581, nVar582, nVar583, nVar584, nVar585, nVar586, nVar587, nVar588, nVar589, nVar590, nVar591, nVar592, nVar593, nVar594, nVar595, nVar596, nVar597, nVar598, nVar599, nVar600, nVar601, nVar602, nVar603, nVar604, nVar605, nVar606, nVar607, nVar608, nVar609, nVar610, nVar611, nVar612, nVar613, nVar614, nVar615, nVar616, nVar617, nVar618, nVar619, nVar620, nVar621, nVar622, nVar623, nVar624, nVar625, nVar626, nVar627, nVar628, nVar629, nVar630, nVar631, nVar632, nVar633, nVar634, nVar635, nVar636, nVar637, nVar638, nVar639, nVar640, nVar641, nVar642, nVar643, nVar644, nVar645, nVar646, nVar647, nVar648, nVar649, nVar650, nVar651, nVar652, nVar653, nVar654, nVar655, nVar656, nVar657, nVar658, nVar659, nVar660, nVar661, nVar662, nVar663, nVar664, nVar665, nVar666, nVar667, nVar668, nVar669, nVar670, nVar671, nVar672, nVar673, nVar674, nVar675, nVar676, nVar677, nVar678, nVar679, nVar680, nVar681, nVar682, nVar683, nVar684, nVar685, nVar686, nVar687, nVar688, nVar689, nVar690, nVar691, nVar692, nVar693, nVar694, nVar695, nVar696, nVar697, nVar698, nVar699, nVar700, nVar701, nVar702, nVar703, nVar704, nVar705, nVar706, nVar707, nVar708, nVar709, nVar710, nVar711, nVar712, nVar713, nVar714, nVar715, nVar716, nVar717, nVar718, nVar719, nVar720, nVar721, nVar722, nVar723, nVar724, nVar725, nVar726, nVar727, nVar728, nVar729, nVar730, nVar731, nVar732, nVar733, nVar734, nVar735, nVar736, nVar737, nVar738, nVar739, nVar740, nVar741, nVar742, nVar743, nVar744, nVar745, nVar746, nVar747, nVar748, nVar749, nVar750, nVar751, nVar752, nVar753, nVar754, nVar755, nVar756, nVar757, nVar758, nVar759, nVar760, nVar761, nVar762, nVar763, nVar764, nVar765, nVar766, nVar767, nVar768, nVar769, nVar770, nVar771, nVar772, nVar773, nVar774, nVar775, nVar776, nVar777, nVar778, nVar779, nVar780, nVar781, nVar782, nVar783, nVar784, nVar785, nVar786, nVar787, nVar788, nVar789, nVar790, nVar791, nVar792, nVar793, nVar794, nVar795, nVar796, nVar797, nVar798, nVar799, nVar800, nVar801, nVar802, nVar803, nVar804, nVar805, nVar806, nVar807, nVar808, nVar809, nVar810, nVar811, nVar812, nVar813, nVar814, nVar815, nVar816, nVar817, nVar818, nVar819, nVar820, nVar821, nVar822, nVar823, nVar824, nVar825, nVar826, nVar827, nVar828, nVar829, nVar830, nVar831, nVar832, nVar833, nVar834, nVar835, nVar836, nVar837, nVar838, nVar839, nVar840, nVar841, nVar842, nVar843, nVar844, nVar845, nVar846, nVar847, nVar848, nVar849, nVar850, nVar851, nVar852, nVar853, nVar854, nVar855, nVar856, nVar857, nVar858, nVar859, nVar860, nVar861, nVar862, nVar863, nVar864, nVar865, nVar866, nVar867, nVar868, nVar869, nVar870, nVar871, nVar872, nVar873, nVar874, nVar875, nVar876, nVar877, nVar878, nVar879, nVar880, nVar881, nVar882, nVar883, nVar884, nVar885, nVar886, nVar887, nVar888, nVar889, nVar890, nVar891, nVar892, nVar893, nVar894, nVar895, nVar896, nVar897, nVar898, nVar899, nVar900, nVar901, nVar902, nVar903, nVar904, nVar905, nVar906, nVar907, nVar908, nVar909, nVar910, nVar911, nVar912, nVar913, nVar914, nVar915, nVar916, nVar917, nVar918, nVar919, nVar920, nVar921, nVar922, nVar923, nVar924, nVar925, nVar926, nVar927, nVar928, nVar929, nVar930, nVar931, nVar932, nVar933, nVar934, nVar935, nVar936, nVar937, nVar938, nVar939, nVar940, nVar941, nVar942, nVar943, nVar944, nVar945, nVar946, nVar947, nVar948, nVar949, nVar950, nVar951, nVar952, nVar953, nVar954, nVar955, nVar956, nVar957, nVar958, nVar959, nVar960, nVar961, nVar962, nVar963, nVar964, nVar965, nVar966, nVar967, nVar968, nVar969, nVar970, nVar971, nVar972, nVar973, nVar974, nVar975, nVar976, nVar977, nVar978, nVar979, nVar980, nVar981, nVar982, nVar983, nVar984, nVar985, nVar986, nVar987, nVar988, nVar989, nVar990, nVar991, nVar992, nVar993, nVar994, nVar995, nVar996, nVar997, nVar998, nVar999, nVar1000, nVar1001, nVar1002, nVar1003, nVar1004, nVar1005, nVar1006, nVar1007, nVar1008, nVar1009, nVar1010, nVar1011, nVar1012, nVar1013, nVar1014, nVar1015, nVar1016, nVar1017, nVar1018, nVar1019, nVar1020, nVar1021, nVar1022, nVar1023, nVar1024, nVar1025, nVar1026, nVar1027, nVar1028, nVar1029, nVar1030, nVar1031, nVar1032, nVar1033, nVar1034, nVar1035, nVar1036, nVar1037, nVar1038, nVar1039, nVar1041, nVar1042, nVar1043, nVar1044, nVar1045, nVar1046, nVar1047, nVar1048, nVar1049, nVar1050, nVar1051, nVar1052, nVar1053, nVar1054, nVar1055, nVar1056, nVar1057, nVar1058, nVar1059, nVar1060, nVar1061, nVar1062, nVar1063, nVar1064, nVar1065, nVar1066, nVar1067, nVar1068, nVar1069, nVar1070, nVar1071, nVar1072, nVar1073, nVar1074, nVar1075, nVar1076, nVar1077, nVar1078, nVar1079, nVar1080, nVar1081, nVar1082, nVar1083, nVar1084, nVar1085, nVar1086, nVar1087, nVar1088, nVar1089, nVar1090, nVar1091, nVar1092, nVar1093, nVar1094, nVar1095, nVar1096, nVar1097, nVar1098, nVar1099, nVar1100, nVar1101, nVar1102, nVar1103, nVar1104, nVar1105, nVar1106, nVar1107, nVar1108, nVar1109, nVar1110, nVar1111, nVar1112, nVar1113, nVar1114, nVar1115, nVar1116, nVar1117, nVar1118, nVar1119, nVar1120, nVar1121, nVar1122, nVar1123, nVar1124, nVar1125, nVar1126, nVar1127, nVar1128, nVar1129, nVar1130, nVar1131, nVar1132, nVar1133, nVar1134, nVar1135, nVar1136, nVar1137, nVar1138, nVar1139, nVar1140, nVar1141, nVar1142, nVar1143, nVar1144, nVar1145, nVar1146, nVar1147, nVar1148, nVar1149, nVar1150, nVar1151, nVar1152, nVar1153, nVar1154, nVar1155, nVar1156, nVar1157, nVar1158, nVar1159, nVar1160, nVar1161, nVar1162, nVar1163, nVar1164, nVar1165, nVar1166, nVar1167, nVar1168, nVar1169, nVar1170, nVar1171, nVar1172, nVar1173, nVar1174, nVar1176, nVar1177, nVar1178, nVar1179, nVar1180, nVar1181, nVar1182, nVar1183, nVar1184, nVar1185, nVar1186, nVar1187, nVar1188, nVar1189, nVar1190, nVar1191, nVar1192, nVar1193, nVar1194, nVar1195, nVar1196, nVar1197, nVar1198, nVar1199, nVar1200, nVar1201, nVar1202, nVar1203, nVar1204, nVar1205, nVar1206, nVar1207, nVar1208, nVar1209, nVar1210, nVar1211, nVar1212, nVar1213, nVar1214, nVar1215, nVar1216, nVar1217, nVar1218, nVar1219, nVar1220, nVar1221, nVar1222, nVar1223, nVar1224, nVar1225, nVar1226, nVar1227, nVar1228, nVar1229, nVar1230, nVar1231, nVar1232, nVar1233, nVar1234, nVar1235, nVar1236, nVar1237, nVar1238, nVar1239, nVar1240, nVar1241, nVar1242, nVar1243, nVar1244, nVar1245, nVar1246, nVar1247, nVar1248, nVar1249, nVar1250, nVar1251, nVar1252, nVar1253, nVar1255, nVar1256, nVar1257, nVar1258, nVar1259, nVar1260, nVar1261, nVar1262, nVar1263, nVar1264, nVar1265, nVar1266, nVar1267, nVar1268, nVar1269, nVar1270, nVar1271, nVar1272, nVar1273, nVar1274, nVar1275, nVar1276, nVar1277, nVar1278, nVar1279, nVar1280, nVar1281, nVar1282, nVar1283, nVar1284, nVar1285, nVar1286, nVar1287, nVar1288, nVar1289, nVar1290, nVar1291, nVar1292, nVar1293, nVar1294, nVar1295, nVar1296, nVar1297, nVar1298, nVar1299, nVar1300, nVar1301, nVar1302, nVar1303, nVar1304, nVar1305, nVar1306, nVar1307, nVar1308, nVar1309, nVar1310, nVar1311, nVar1312, nVar1313, nVar1314, nVar1315, nVar1316, nVar1317, nVar1318, nVar1319, nVar1320, nVar1321, nVar1322, nVar1323, nVar1324, nVar1325, nVar1326, nVar1327, nVar1328, nVar1329, nVar1330, nVar1331, nVar1332, nVar1333, nVar1334, nVar1335, nVar1336, nVar1337, nVar1338, nVar1339, nVar1340, nVar1341, nVar1342, nVar1343, nVar1344, nVar1345, nVar1346, nVar1347, nVar1348, nVar1349, nVar1350, nVar1351, nVar1352, nVar1353, nVar1354, nVar1355, nVar1356, nVar1357, nVar1358, nVar1359, nVar1360, nVar1361, nVar1362, nVar1363, nVar1364, nVar1365, nVar1366, nVar1367, nVar1368, nVar1369, nVar1370, nVar1371, nVar1372, nVar1373, nVar1374, nVar1375, nVar1376, nVar1377, nVar1378, nVar1379, nVar1380, nVar1381, nVar1382, nVar1383, nVar1384, nVar1385, nVar1386, nVar1387, nVar1388, nVar1389, nVar1390, nVar1391, nVar1392, nVar1393, nVar1394, nVar1395, nVar1396, nVar1397, nVar1398, nVar1399, nVar1400, nVar1401, nVar1402, nVar1403, nVar1404, nVar1405, nVar1406, nVar1407, nVar1408, nVar1409, nVar1410, nVar1411, nVar1412, nVar1413, nVar1414, nVar1415, nVar1416, nVar1417, nVar1418, nVar1419, nVar1420, nVar1421, nVar1422, nVar1423, nVar1424, nVar1425, nVar1426, nVar1427, nVar1428, nVar1429, nVar1430, nVar1431, nVar1432, nVar1433, nVar1434, nVar1435, nVar1436, nVar1437, nVar1438, nVar1439, nVar1440, nVar1441, nVar1442, nVar1443, nVar1444, nVar1445, nVar1446, nVar1447, nVar1448, nVar1449, nVar1450, nVar1451, nVar1452, nVar1453, nVar1454, nVar1455, nVar1456, nVar1457, nVar1458, nVar1459, nVar1460, nVar1461, nVar1462, nVar1463, nVar1464, nVar1465, nVar1466, nVar1467, nVar1468, nVar1469, nVar1470, nVar1471, nVar1472, nVar1473, nVar1474, nVar1475, nVar1476, nVar1477, nVar1478, nVar1479, nVar1480, nVar1481, nVar1482, nVar1483, nVar1484, nVar1485, nVar1486, nVar1487, nVar1488, nVar1489, nVar1490, nVar1491, nVar1492, nVar1493, nVar1494, nVar1495, nVar1496, nVar1497, nVar1498, nVar1499, nVar1500, nVar1501, nVar1502, nVar1503, nVar1504, nVar1505, nVar1506, nVar1507, nVar1508, nVar1509, nVar1510, nVar1511, nVar1512, nVar1513, nVar1514, nVar1515, nVar1516, nVar1517, nVar1518, nVar1519, nVar1520, nVar1521, nVar1522, nVar1523, nVar1524, nVar1525, nVar1526, nVar1527, nVar1528, nVar1529, nVar1530, nVar1531, nVar1532, nVar1533, nVar1534, nVar1535, nVar1536, nVar1537, nVar1538, nVar1539, nVar1540, nVar1541, nVar1542, nVar1543, nVar1544, nVar1545, nVar1546, nVar1547, nVar1548, nVar1549, nVar1550, nVar1551, nVar1552, nVar1553, nVar1554, nVar1555, nVar1556, nVar1557, nVar1558, nVar1559, nVar1560, nVar1561, nVar1562, nVar1563, nVar1564, nVar1565, nVar1566, nVar1567, nVar1568, nVar1569, nVar1570, nVar1571, nVar1572, nVar1573, nVar1574, nVar1575, nVar1576, nVar1577, nVar1578, nVar1579, nVar1580, nVar1581, nVar1582, nVar1583, nVar1584, nVar1585, nVar1586, nVar1587, nVar1588, nVar1589, nVar1590, nVar1591, nVar1592, nVar1593, nVar1594, nVar1595, nVar1596, nVar1597, nVar1598, nVar1599, nVar1600, nVar1601, nVar1602, nVar1603, nVar1604, nVar1605, nVar1606, nVar1607, nVar1608, nVar1609, nVar1610, nVar1611, nVar1612, nVar1613, nVar1614, nVar1615, nVar1616, nVar1617, nVar1618, nVar1619, nVar1620, nVar1621, nVar1622, nVar1623, nVar1624, nVar1625, nVar1626, nVar1627, nVar1628, nVar1629, nVar1630, nVar1631, nVar1632, nVar1633, nVar1634, nVar1635, nVar1636, nVar1637, nVar1638, nVar1639, nVar1640, nVar1641, nVar1642, nVar1643, nVar1644, nVar1645, nVar1646, nVar1647, nVar1648, nVar1649, nVar1650, nVar1651, nVar1652, nVar1653, nVar1654, nVar1655, nVar1656, nVar1657, nVar1658, nVar1659, nVar1660, nVar1661, nVar1662, nVar1663, nVar1664, nVar1665, nVar1666, nVar1667, nVar1668, nVar1669, nVar1670, nVar1671, nVar1672, nVar1673, nVar1674, nVar1675, nVar1676, nVar1677, nVar1678, nVar1679, nVar1680, nVar1681, nVar1682, nVar1683, nVar1684, nVar1685, nVar1686, nVar1687, nVar1688, nVar1689, nVar1690, nVar1691, nVar1692, nVar1693, nVar1694, nVar1695, nVar1696, nVar1697, nVar1698, nVar1699, nVar1700, nVar1701, nVar1702, nVar1703, nVar1704, nVar1705, nVar1706, nVar1707, nVar1708, nVar1709, nVar1710, nVar1711, nVar1712, nVar1713, nVar1714, nVar1715, nVar1716, nVar1717, nVar1718, nVar1719, nVar1720, nVar1721, nVar1722, nVar1723, nVar1724, nVar1725, nVar1726, nVar1727, nVar1728, nVar1729, nVar1730, nVar1731, nVar1732, nVar1733, nVar1734, nVar1735, nVar1736, nVar1737, nVar1738, nVar1739, nVar1740, nVar1741, nVar1742, nVar1743, nVar1744, nVar1745, nVar1746, nVar1747, nVar1748, nVar1749, nVar1750, nVar1751, nVar1752, nVar1753, nVar1754, nVar1755, nVar1756, nVar1757, nVar1758, nVar1759, nVar1760, nVar1761, nVar1762, nVar1763, nVar1764, nVar1765, nVar1766, nVar1767, nVar1768, nVar1769, nVar1770, nVar1771, nVar1772, nVar1773, nVar1774, nVar1775, nVar1776, nVar1777, nVar1778, nVar1779, nVar1780, nVar1781, nVar1782, nVar1783, nVar1784, nVar1785, nVar1786, nVar1787, nVar1788, nVar1789, nVar1790, nVar1791, nVar1792, nVar1793, nVar1794, nVar1795, nVar1796, nVar1797, nVar1798, nVar1799, nVar1800, nVar1801, nVar1802, nVar1803, nVar1804, nVar1805, nVar1806, nVar1807, nVar1808, nVar1809, nVar1810, nVar1811, nVar1812, nVar1813, nVar1814, nVar1815, nVar1816, nVar1817, nVar1818, nVar1819, nVar1820, nVar1821, nVar1822, nVar1823, nVar1824, nVar1825, nVar1826, nVar1827, nVar1828, nVar1829, nVar1830, nVar1831, nVar1832, nVar1833, nVar1834, nVar1835, nVar1836, nVar1837, nVar1838, nVar1839, nVar1840, nVar1841, nVar1842, nVar1843, nVar1844, nVar1845, nVar1846, nVar1847, nVar1848, nVar1849, nVar1850, nVar1851, nVar1852, nVar1853, nVar1854, nVar1855, nVar1856, nVar1857, nVar1858, nVar1859, nVar1860, nVar1861, nVar1862, nVar1863, nVar1864, nVar1865, nVar1866, nVar1867, nVar1868, nVar1869, nVar1870, nVar1871, nVar1872, nVar1873, nVar1874, nVar1875, nVar1876, nVar1877, nVar1878, nVar1879, nVar1880, nVar1881, nVar1882, nVar1883, nVar1884, nVar1885, nVar1886, nVar1887, nVar1888, nVar1889, nVar1890, nVar1891, nVar1892, nVar1893, nVar1894, nVar1895, nVar1896, nVar1897, nVar1898, nVar1899, nVar1900, nVar1901, nVar1902, nVar1903, nVar1904, nVar1905, nVar1906, nVar1907, nVar1908, nVar1909, nVar1910, nVar1911, nVar1912, nVar1913, nVar1914, nVar1915, nVar1916, nVar1917, nVar1918, nVar1919, nVar1920, nVar1921, nVar1922, nVar1923, nVar1924, nVar1925, nVar1926, nVar1928, nVar1929, nVar1930, nVar1931, nVar1932, nVar1933, nVar1934, nVar1935, nVar1936, nVar1937, nVar1938, nVar1939, nVar1940, nVar1941, nVar1942, nVar1943, nVar1944, nVar1945, nVar1946, nVar1947, nVar1948, nVar1949, nVar1950, nVar1951, nVar1952, nVar1953, nVar1954, nVar1955, nVar1956, nVar1957, nVar1958, nVar1959, nVar1960, nVar1961, nVar1962, nVar1963, nVar1964, nVar1965, nVar1966, nVar1967, nVar1968, nVar1969, nVar1970, nVar1971, nVar1972, nVar1973, nVar1974, nVar1975, nVar1976, nVar1977, nVar1978, nVar1979, nVar1980, nVar1981, nVar1982, nVar1983, nVar1984, nVar1985, nVar1986, nVar1987, nVar1988, nVar1989, nVar1990, nVar1991, nVar1992, nVar1993, nVar1994, nVar1995, nVar1996, nVar1997, nVar1998, nVar1999, nVar2000, nVar2001, nVar2002, nVar2003, nVar2004, nVar2005, nVar2006, nVar2007, nVar2008, nVar2009, nVar2010, nVar2011, nVar2012, nVar2013, nVar2014, nVar2015, nVar2016, nVar2017, nVar2018, nVar2019, nVar2020, nVar2021, nVar2022, nVar2023, nVar2024, nVar2025, nVar2026, nVar2027, nVar2028, nVar2029, nVar2030, nVar2031, nVar2032, nVar2033, nVar2034, nVar2035, nVar2036, nVar2037, nVar2038, nVar2039, nVar2040, nVar2041, nVar2042, nVar2043, nVar2044, nVar2045, nVar2046, nVar2047, nVar2048, nVar2049, nVar2050, nVar2051, nVar2052, nVar2053, nVar2054, nVar2055, nVar2056, nVar2057, nVar2058, nVar2059, nVar2060, nVar2061, nVar2062, nVar2063, nVar2064, nVar2065, nVar2066, nVar2067, nVar2068, nVar2069, nVar2070, nVar2071, nVar2072, nVar2073, nVar2074, nVar2075, nVar2076, nVar2077, nVar2078, nVar2079, nVar2080, nVar2081, nVar2082, nVar2083, nVar2084, nVar2085, nVar2086, nVar2087, nVar2088, nVar2089, nVar2090, nVar2091, nVar2092, nVar2093, nVar2094, nVar2095, nVar2096, nVar2097, nVar2098, nVar2099, nVar2100, nVar2101, nVar2102, nVar2104, nVar2105, nVar2106, nVar2107, nVar2108, nVar2109, nVar2110, nVar2111, nVar2112, nVar2113, nVar2114, nVar2115, nVar2116, nVar2117, nVar2118, nVar2119, nVar2120, nVar2121, nVar2122, nVar2123, nVar2124, nVar2125, nVar2126, nVar2127, nVar2128, nVar2129, nVar2130, nVar2131, nVar2132, nVar2133, nVar2134, nVar2135, nVar2136, nVar2137, nVar2138, nVar2139, nVar2140, nVar2141, nVar2142, nVar2143, nVar2144, nVar2145, nVar2146, nVar2147, nVar2148, nVar2149, nVar2150, nVar2151, nVar2152, nVar2153, nVar2154, nVar2155, nVar2156, nVar2157, nVar2158, nVar2159, nVar2160, nVar2161, nVar2162, nVar2163, nVar2164, nVar2165, nVar2166, nVar2167, nVar2168, nVar2169, nVar2170, nVar2171, nVar2172, nVar2173, nVar2174, nVar2175, nVar2176, nVar2177, nVar2178, nVar2180, nVar2181, nVar2182, nVar2183, nVar2184, nVar2185, nVar2186, nVar2187, nVar2188, nVar2189, nVar2190, nVar2191, nVar2192, nVar2193, nVar2194, nVar2195, nVar2196, nVar2197, nVar2198, nVar2199, nVar2200, nVar2201, nVar2202, nVar2203, nVar2204, nVar2205, nVar2206, nVar2207, nVar2208, nVar2209, nVar2210, nVar2211, nVar2212, nVar2213, nVar2214, nVar2215, nVar2216, nVar2217, nVar2218, nVar2219, nVar2220, nVar2221, nVar2222, nVar2223, nVar2224, nVar2225, nVar2226, nVar2227, nVar2228, nVar2229, nVar2230, nVar2231, nVar2232, nVar2233, nVar2234, nVar2235, nVar2236, nVar2237, nVar2238, nVar2239, nVar2240, nVar2241, nVar2242, nVar2243, nVar2244, nVar2245, nVar2246, nVar2247, nVar2248, nVar2249, nVar2250, nVar2251, nVar2252, nVar2253, nVar2254, nVar2255, nVar2256, nVar2257, nVar2258, nVar2259, nVar2260, nVar2261, nVar2262, nVar2263, nVar2264, nVar2265, nVar2266, nVar2267, nVar2268, nVar2269, nVar2270, nVar2271, nVar2272, nVar2273, nVar2274, nVar2275, nVar2276, nVar2277, nVar2278, nVar2279, nVar2280, nVar2281, nVar2282, nVar2283, nVar2284, nVar2285, nVar2286, nVar2287, nVar2288, nVar2289, nVar2290, nVar2291, nVar2292, nVar2293, nVar2294, nVar2295, nVar2296, nVar2297, nVar2298, nVar2299, nVar2300, nVar2301, nVar2302, nVar2303, nVar2304, nVar2305, nVar2306, nVar2307, nVar2308, nVar2309, nVar2310, nVar2311, nVar2312, nVar2313, nVar2314, nVar2315, nVar2316, nVar2317, nVar2318, nVar2319, nVar2320, nVar2321, nVar2322, nVar2323, nVar2324, nVar2325, nVar2326, nVar2327, nVar2328, nVar2329, nVar2330, nVar2331, nVar2332, nVar2333, nVar2334, nVar2335, nVar2336, nVar2337, nVar2338, nVar2339, nVar2340, nVar2341, nVar2342, nVar2343, nVar2344, nVar2345, nVar2346, nVar2347, nVar2348, nVar2349, nVar2350, nVar2351, nVar2352, nVar2353, nVar2354, nVar2355, nVar2356, nVar2357, nVar2358, nVar2359, nVar2360, nVar2361, nVar2362, nVar2363, nVar2364, nVar2365, nVar2366, nVar2367, nVar2368, nVar2369, nVar2370, nVar2371, nVar2372, nVar2373, nVar2374, nVar2375, nVar2376, nVar2377, nVar2378, nVar2379, nVar2380, nVar2381, nVar2382, nVar2383, nVar2384, nVar2385, nVar2386, nVar2387, nVar2388, nVar2389, nVar2390, nVar2391, nVar2392, nVar2393, nVar2394, nVar2395, nVar2396, nVar2397, nVar2398, nVar2399, nVar2400, nVar2401, nVar2402, nVar2403, nVar2404, nVar2405, nVar2406, nVar2407, nVar2408, nVar2409, nVar2410, nVar2411, nVar2412, nVar2413, nVar2414, nVar2415, nVar2416, nVar2417, nVar2418, nVar2419, nVar2420, nVar2421, nVar2422, nVar2423, nVar2424, nVar2425, nVar2426, nVar2427, nVar2428, nVar2429, nVar2430, nVar2431, nVar2432, nVar2433, nVar2434, nVar2435, nVar2436, nVar2437, nVar2438, nVar2439, nVar2440, nVar2441, nVar2442, nVar2443, nVar2444, nVar2445, nVar2446, nVar2447, nVar2448, nVar2449, nVar2450, nVar2451, nVar2452, nVar2453, nVar2454, nVar2455, nVar2456, nVar2457, nVar2458, nVar2459, nVar2460, nVar2461, nVar2462, nVar2463, nVar2464, nVar2465, nVar2466, nVar2467, nVar2468, nVar2469, nVar2470, nVar2471, nVar2472, nVar2473, nVar2474, nVar2475, nVar2476, nVar2477, nVar2478, nVar2479, nVar2480, nVar2481, nVar2482, nVar2483, nVar2484, nVar2485, nVar2486, nVar2487, nVar2488, nVar2489, nVar2490, nVar2491, nVar2492, nVar2493, nVar2494, nVar2495, nVar2496, nVar2497, nVar2498, nVar2499, nVar2500, nVar2501, nVar2502, nVar2503, nVar2504, nVar2505, nVar2506, nVar2507, nVar2508, nVar2509, nVar2510, nVar2511, nVar2512, nVar2513, nVar2514, nVar2515, nVar2516, nVar2517, nVar2518, nVar2519, nVar2520, nVar2521, nVar2522, nVar2523, nVar2524, nVar2525, nVar2526, nVar2527, nVar2528, nVar2529, nVar2530, nVar2531, nVar2532, nVar2533, nVar2534, nVar2535, nVar2536, nVar2537, nVar2538, nVar2539, nVar2540, nVar2541, nVar2542, nVar2543, nVar2544, nVar2545, nVar2546, nVar2547, nVar2548, nVar2549, nVar2550, nVar2551, nVar2552, nVar2553, nVar2554, nVar2555, nVar2556, nVar2557, nVar2558, nVar2559, nVar2560, nVar2561, nVar2562, nVar2563, nVar2564, nVar2565, nVar2566, nVar2567, nVar2568, nVar2569, nVar2570, nVar2571, nVar2572, nVar2573, nVar2574, nVar2575, nVar2576, nVar2577, nVar2578, nVar2579, nVar2580, nVar2581, nVar2582, nVar2583, nVar2584, nVar2585, nVar2586, nVar2587, nVar2588, nVar2589, nVar2590, nVar2591, nVar2592, nVar2593, nVar2594, nVar2595, nVar2596, nVar2597, nVar2598, nVar2599, nVar2600, nVar2601, nVar2602, nVar2603, nVar2604, nVar2605, nVar2606, nVar2607, nVar2608, nVar2609, nVar2610, nVar2611, nVar2612, nVar2613, nVar2614, nVar2615, nVar2616, nVar2617, nVar2618, nVar2619, nVar2620, nVar2622, nVar2623, nVar2624, nVar2625, nVar2626, nVar2627, nVar2628, nVar2629, nVar2630, nVar2631, nVar2633, nVar2634, nVar2635, nVar2636, nVar2637, nVar2638, nVar2639, nVar2640, nVar2641, nVar2642, nVar2643, nVar2644, nVar2645, nVar2646, nVar2647, nVar2648, nVar2649, nVar2650, nVar2651, nVar2652, nVar2653, nVar2654, nVar2655, nVar2656, nVar2657, nVar2658, nVar2659, nVar2660, nVar2661, nVar2662, nVar2663, nVar2664, nVar2665, nVar2666, nVar2667, nVar2668, nVar2669, nVar2670, nVar2671, nVar2672, nVar2673, nVar2674, nVar2675, nVar2676, nVar2677, nVar2678, nVar2679, nVar2680, nVar2681, nVar2682, nVar2683, nVar2684, nVar2685, nVar2686, nVar2687, nVar2688, nVar2689, nVar2690, nVar2691, nVar2692, nVar2693, nVar2694, nVar2695, nVar2696, nVar2697, nVar2698, nVar2699, nVar2700, nVar2701, nVar2702, nVar2703, nVar2704, nVar2705, nVar2706, nVar2707, nVar2708, nVar2709, nVar2710, nVar2711, nVar2712, nVar2713, nVar2714, nVar2715, nVar2716, nVar2717, nVar2718, nVar2719, nVar2720, nVar2721, nVar2722, nVar2723, nVar2724, nVar2725, nVar2726, nVar2727, nVar2728, nVar2729, nVar2730, nVar2731, nVar2732, nVar2733, nVar2734, nVar2735, nVar2736, nVar2737, nVar2738, nVar2739, nVar2740, nVar2741, nVar2742, nVar2743, nVar2744, nVar2745, nVar2746, nVar2747, nVar2748, nVar2749, nVar2750, nVar2751, nVar2752, nVar2753, nVar2755, nVar2756, nVar2757, nVar2758, nVar2759, nVar2760, nVar2761, nVar2762, nVar2763, nVar2764, nVar2765, nVar2766, nVar2767, nVar2768, nVar2769, nVar2770, nVar2771, nVar2772, nVar2773, nVar2774, nVar2775, nVar2776, nVar2777, nVar2778, nVar2779, nVar2780, nVar2781, nVar2782, nVar2783, nVar2784, nVar2785, nVar2786, nVar2787, nVar2788, nVar2789, nVar2790, nVar2791, nVar2792, nVar2793, nVar2794, nVar2795, nVar2796, nVar2797, nVar2798, nVar2799, nVar2800, nVar2801, nVar2802, nVar2803, nVar2804, nVar2805, nVar2806, nVar2807, nVar2808, nVar2809, nVar2810, nVar2811, nVar2812, nVar2813, nVar2814, nVar2815, nVar2816, nVar2817, nVar2818, nVar2819, nVar2820, nVar2821, nVar2822, nVar2823, nVar2824, nVar2825, nVar2826, nVar2827, nVar2828, nVar2829, nVar2830, nVar2831, nVar2832, nVar2833, nVar2834, nVar2835, nVar2836, nVar2837, nVar2838, nVar2839, nVar2840, nVar2841, nVar2842, nVar2843, nVar2844, nVar2845, nVar2846, nVar2847, nVar2848, nVar2849, nVar2850, nVar2851, nVar2852, nVar2853, nVar2854, nVar2855, nVar2856, nVar2857, nVar2858, nVar2859, nVar2860, nVar2861, nVar2862, nVar2863, nVar2864, nVar2865, nVar2866, nVar2867, nVar2868, nVar2869, nVar2870, nVar2871, nVar2872, nVar2873, nVar2874, nVar2875, nVar2876, nVar2877, nVar2878, nVar2879, nVar2880, nVar2881, nVar2882, nVar2883, nVar2884, nVar2885, nVar2886, nVar2887, nVar2888, nVar2889, nVar2890, nVar2891, nVar2892, nVar2893, nVar2894, nVar2895, nVar2896, nVar2897, nVar2898, nVar2899, nVar2900, nVar2901, nVar2902, nVar2903, nVar2904, nVar2905, nVar2906, nVar2907, nVar2908, nVar2909, nVar2910, nVar2911, nVar2912, nVar2913, nVar2914, nVar2915, nVar2916, nVar2917, nVar2918, nVar2919, nVar2920, nVar2921, nVar2922, nVar2923, nVar2924, nVar2925, nVar2926, nVar2927, nVar2928, nVar2929, nVar2930, nVar2931, nVar2932, nVar2933, nVar2934, nVar2935, nVar2936, nVar2937, nVar2938, nVar2939, nVar2940, nVar2941, nVar2942, nVar2943, nVar2944, nVar2945, nVar2946, nVar2947, nVar2948, nVar2949, nVar2950, nVar2951, nVar2952, nVar2953, nVar2954, nVar2955, nVar2956, nVar2957, nVar2958, nVar2959, nVar2960, nVar2961, nVar2962, nVar2963, nVar2964, nVar2965, nVar2966, nVar2967, nVar2968, nVar2969, nVar2970, nVar2971, nVar2972, nVar2973, nVar2974, nVar2975, nVar2976, nVar2977, nVar2978, nVar2979, nVar2980, nVar2981, nVar2982, nVar2983, nVar2984, nVar2985, nVar2986, nVar2987, nVar2988, nVar2989, nVar2990, nVar2991, nVar2992, nVar2993, nVar2994, nVar2995, nVar2996, nVar2997, nVar2998, nVar2999, nVar3000, nVar3001, nVar3002, nVar3003, nVar3004, nVar3005, nVar3006, nVar3007, nVar3008, nVar3009, nVar3010, nVar3011, nVar3012, nVar3013, nVar3014, nVar3015, nVar3016, nVar3017, nVar3018, nVar3019, nVar3020, nVar3021, nVar3022, nVar3023, nVar3024, nVar3025, nVar3026, nVar3027, nVar3028, nVar3029, nVar3030, nVar3031, nVar3032, nVar3033, nVar3034, nVar3035, nVar3036, nVar3037, nVar3038, nVar3039, nVar3040, nVar3041, nVar3042, nVar3043, nVar3044, nVar3045, nVar3046, nVar3047, nVar3049, nVar3050, nVar3051, nVar3052, nVar3053, nVar3054, nVar3055, nVar3056, nVar3057, nVar3058, nVar3059, nVar3060, nVar3061, nVar3063, nVar3064, nVar3065, nVar3066, nVar3067, nVar3068, nVar3069, nVar3070, nVar3071, nVar3072, nVar3073, nVar3074, nVar3075, nVar3076, nVar3077, nVar3078, nVar3079, nVar3080, nVar3081, nVar3082, nVar3083, nVar3084, nVar3085, nVar3086, nVar3087, nVar3088, nVar3089, nVar3090, nVar3091, nVar3092, nVar3093, nVar3094, nVar3095, nVar3096, nVar3097, nVar3098, nVar3099, nVar3100, nVar3101, nVar3102, nVar3103, nVar3104, nVar3105, nVar3106, nVar3107, nVar3108, nVar3109, nVar3110, nVar3111, nVar3112, nVar3113, nVar3114, nVar3115, nVar3116, nVar3117, nVar3118, nVar3119, nVar3120, nVar3121, nVar3122, nVar3123, nVar3124, nVar3125, nVar3126, nVar3127, nVar3128, nVar3129, nVar3130, nVar3131, nVar3132, nVar3133, nVar3134, nVar3135, nVar3136, nVar3137, nVar3138, nVar3140, nVar3141, nVar3142, nVar3143, nVar3144, nVar3145, nVar3146, nVar3147, nVar3148, nVar3149, nVar3150, nVar3151, nVar3152, nVar3153, nVar3154, nVar3155, nVar3156, nVar3157, nVar3158, nVar3159, nVar3160, nVar3161, nVar3162, nVar3163, nVar3164, nVar3165, nVar3166, nVar3167, nVar3168, nVar3169, nVar3170, nVar3171, nVar3172, nVar3173, nVar3174, nVar3175, nVar3176, nVar3177, nVar3178, nVar3179, nVar3180, nVar3181, nVar3182, nVar3183, nVar3184, nVar3185, nVar3186, nVar3187, nVar3188, nVar3189, nVar3190, nVar3191, nVar3192, nVar3193, nVar3194, nVar3195, nVar3196, nVar3197, nVar3198, nVar3199, nVar3200, nVar3201, nVar3202, nVar3203, nVar3204, nVar3205, nVar3206, nVar3207, nVar3208, nVar3209, nVar3210, nVar3211, nVar3212, nVar3213, nVar3214, nVar3215, nVar3216, nVar3217, nVar3218, nVar3219, nVar3220, nVar3221, nVar3222, nVar3223, nVar3224, nVar3225, nVar3226, nVar3227, nVar3228, nVar3229, nVar3230, nVar3231, nVar3232, nVar3233, nVar3234, nVar3235, nVar3236, nVar3237, nVar3238, nVar3239, nVar3240, nVar3241, nVar3242, nVar3243, nVar3244, nVar3245, nVar3246, nVar3247, nVar3248, nVar3249, nVar3250, nVar3251, nVar3252, nVar3253, nVar3254, nVar3255, nVar3256, nVar3257, nVar3258, nVar3259, nVar3260, nVar3261, nVar3262, nVar3263, nVar3264, nVar3265, nVar3266, nVar3267, nVar3268, nVar3269, nVar3270, nVar3271, nVar3272, nVar3273, nVar3274, nVar3275, nVar3276, nVar3277, nVar3278, nVar3279, nVar3280, nVar3281, nVar3282, nVar3283, nVar3284, nVar3285, nVar3286, nVar3287, nVar3288, nVar3289, nVar3290, nVar3291, nVar3292, nVar3293, nVar3294, nVar3295, nVar3296, nVar3297, nVar3298, nVar3299, nVar3300, nVar3301, nVar3302, nVar3303, nVar3304, nVar3305, nVar3306, nVar3307, nVar3308, nVar3309, nVar3310, nVar3311, nVar3312, nVar3313, nVar3314, nVar3315, nVar3316, nVar3317, nVar3318, nVar3319, nVar3320, nVar3321, nVar3322, nVar3323, nVar3324, nVar3325, nVar3326, nVar3327, nVar3328, nVar3329, nVar3330, nVar3331, nVar3332, nVar3333, nVar3334, nVar3335, nVar3336, nVar3337, nVar3338, nVar3339, nVar3340, nVar3341, nVar3342, nVar3343, nVar3344, nVar3345, nVar3346, nVar3347, nVar3348, nVar3349, nVar3350, nVar3351, nVar3352, nVar3353, nVar3354, nVar3355, nVar3356, nVar3357, nVar3358, nVar3359, nVar3360, nVar3361, nVar3362, nVar3363, nVar3364, nVar3365, nVar3366, nVar3367, nVar3368, nVar3369, nVar3370, nVar3371, nVar3372, nVar3373, nVar3374, nVar3375, nVar3376, nVar3377, nVar3378, nVar3379, nVar3380, nVar3381, nVar3382, nVar3383, nVar3384, nVar3385, nVar3386, nVar3387, nVar3388, nVar3389, nVar3390, nVar3391, nVar3392, nVar3393, nVar3394, nVar3395, nVar3396, nVar3397, nVar3398, nVar3399, nVar3400, nVar3401, nVar3402, nVar3403, nVar3404, nVar3405, nVar3406, nVar3407, nVar3408, nVar3409, nVar3410, nVar3411, nVar3412, nVar3413, nVar3414, nVar3415, nVar3416, nVar3417, nVar3418, nVar3419, nVar3420, nVar3421, nVar3422, nVar3423, nVar3424, nVar3425, nVar3426, nVar3427, nVar3428, nVar3429, nVar3430, nVar3431, nVar3432, nVar3433, nVar3434, nVar3435, nVar3436, nVar3437, nVar3438, nVar3439, nVar3440, nVar3441, nVar3442, nVar3443, nVar3444, nVar3445, nVar3446, nVar3447, nVar3448, nVar3449, nVar3450, nVar3451, nVar3452, nVar3453, nVar3454, nVar3455, nVar3456, nVar3457, nVar3458, nVar3459, nVar3460, nVar3461, nVar3462, nVar3463, nVar3464, nVar3465, nVar3466, nVar3467, nVar3468, nVar3469, nVar3470, nVar3471, nVar3472, nVar3473, nVar3474, nVar3475, nVar3476, nVar3477, nVar3478, nVar3479, nVar3480, nVar3481, nVar3482, nVar3483, nVar3484, nVar3485, nVar3486, nVar3487, nVar3488, nVar3489, nVar3490, nVar3491, nVar3492, nVar3493, nVar3494, nVar3495, nVar3496, nVar3497, nVar3498, nVar3499, nVar3500, nVar3501, nVar3502, nVar3503, nVar3504, nVar3505, nVar3506, nVar3507, nVar3508, nVar3509, nVar3510, nVar3511, nVar3512, nVar3513, nVar3514, nVar3515, nVar3516, nVar3517, nVar3518, nVar3519, nVar3520, nVar3521, nVar3522, nVar3523, nVar3524, nVar3525, nVar3526, nVar3527, nVar3528, nVar3529, nVar3530, nVar3531, nVar3532, nVar3533, nVar3534, nVar3535, nVar3536, nVar3537, nVar3538, nVar3539, nVar3540, nVar3541, nVar3542, nVar3543, nVar3544, nVar3545, nVar3546, nVar3547, nVar3548, nVar3549, nVar3550, nVar3551, nVar3552, nVar3553, nVar3554, nVar3555, nVar3556, nVar3557, nVar3558, nVar3559, nVar3560, nVar3561, nVar3562, nVar3563, nVar3564, nVar3565, nVar3566, nVar3567, nVar3568, nVar3569, nVar3570, nVar3571, nVar3572, nVar3573, nVar3574, nVar3575, nVar3576, nVar3577, nVar3578, nVar3579, nVar3580, nVar3581, nVar3582, nVar3583, nVar3584, nVar3585, nVar3586, nVar3587, nVar3588, nVar3589, nVar3590, nVar3591, nVar3592, nVar3593, nVar3594, nVar3595, nVar3596, nVar3597, nVar3598, nVar3599, nVar3600, nVar3601, nVar3602, nVar3603, nVar3604, nVar3605, nVar3606, nVar3607, nVar3608, nVar3609, nVar3610, nVar3611, nVar3612, nVar3613, nVar3614, nVar3615, nVar3616, nVar3617, nVar3618, nVar3619, nVar3620, nVar3621, nVar3622, nVar3623, nVar3624, nVar3625, nVar3626, nVar3627, nVar3628, nVar3629, nVar3630, nVar3631, nVar3632, nVar3633, nVar3634, nVar3635, nVar3636, nVar3637, nVar3638, nVar3639, nVar3640, nVar3641, nVar3642, nVar3643, nVar3644, nVar3645, nVar3646, nVar3647, nVar3648, nVar3649, nVar3650, nVar3651, nVar3652, nVar3653, nVar3654, nVar3655, nVar3656, nVar3657, nVar3658, nVar3659, nVar3660, nVar3661, nVar3662, nVar3663, nVar3664, nVar3665, nVar3666, nVar3667, nVar3668, nVar3669, nVar3670, nVar3671, nVar3672, nVar3673, nVar3674, nVar3675, nVar3676, nVar3677, nVar3678, nVar3679, nVar3680, nVar3681, nVar3682, nVar3683, nVar3684, nVar3685, nVar3686, nVar3687, nVar3688, nVar3689, nVar3690, nVar3691, nVar3692, nVar3693, nVar3694, nVar3695, nVar3696, nVar3697, nVar3698, nVar3699, nVar3700, nVar3701, nVar3702, nVar3703, nVar3704, nVar3705, nVar3706, nVar3707, nVar3708, nVar3709, nVar3710, nVar347, nVar399, nVar1040, nVar1175, nVar2103, nVar2179, nVar2621, nVar2632, nVar2754, nVar3048, nVar3062, nVar3139, nVar3711, nVar3714, nVar3717, nVar3722, nVar3721, nVar1254, nVar280, nVar3718, nVar3719, nVar3720;
diff --git a/Test/stratifiedinline/large.bpl.expect b/Test/stratifiedinline/large.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/stratifiedinline/large.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors |