From 73a1c73067c3664187d2cc98e5b6abc04b6691c2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 20:45:05 +0100 Subject: 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 --- Test/stratifiedinline/Answer | 454 ++++++++++++++++----------------- Test/stratifiedinline/bar1.bpl | 2 + Test/stratifiedinline/bar1.bpl.expect | 14 + Test/stratifiedinline/bar10.bpl | 4 +- Test/stratifiedinline/bar10.bpl.expect | 97 +++++++ Test/stratifiedinline/bar11.bpl | 2 + Test/stratifiedinline/bar11.bpl.expect | 18 ++ Test/stratifiedinline/bar12.bpl | 2 + Test/stratifiedinline/bar12.bpl.expect | 5 + Test/stratifiedinline/bar13.bpl | 2 + Test/stratifiedinline/bar13.bpl.expect | 2 + Test/stratifiedinline/bar2.bpl | 2 + Test/stratifiedinline/bar2.bpl.expect | 13 + Test/stratifiedinline/bar3.bpl | 2 + Test/stratifiedinline/bar3.bpl.expect | 21 ++ Test/stratifiedinline/bar4.bpl | 2 + Test/stratifiedinline/bar4.bpl.expect | 2 + Test/stratifiedinline/bar6.bpl | 2 + Test/stratifiedinline/bar6.bpl.expect | 2 + Test/stratifiedinline/bar7.bpl | 4 +- Test/stratifiedinline/bar7.bpl.expect | 91 +++++++ Test/stratifiedinline/bar8.bpl | 4 +- Test/stratifiedinline/bar8.bpl.expect | 91 +++++++ Test/stratifiedinline/bar9.bpl | 4 +- Test/stratifiedinline/bar9.bpl.expect | 135 ++++++++++ Test/stratifiedinline/large.bpl | 2 + Test/stratifiedinline/large.bpl.expect | 2 + 27 files changed, 750 insertions(+), 231 deletions(-) create mode 100644 Test/stratifiedinline/bar1.bpl.expect create mode 100644 Test/stratifiedinline/bar10.bpl.expect create mode 100644 Test/stratifiedinline/bar11.bpl.expect create mode 100644 Test/stratifiedinline/bar12.bpl.expect create mode 100644 Test/stratifiedinline/bar13.bpl.expect create mode 100644 Test/stratifiedinline/bar2.bpl.expect create mode 100644 Test/stratifiedinline/bar3.bpl.expect create mode 100644 Test/stratifiedinline/bar4.bpl.expect create mode 100644 Test/stratifiedinline/bar6.bpl.expect create mode 100644 Test/stratifiedinline/bar7.bpl.expect create mode 100644 Test/stratifiedinline/bar8.bpl.expect create mode 100644 Test/stratifiedinline/bar9.bpl.expect create mode 100644 Test/stratifiedinline/large.bpl.expect (limited to 'Test/stratifiedinline') 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 -- cgit v1.2.3