summaryrefslogtreecommitdiff
path: root/Test/stratifiedinline/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/stratifiedinline/Answer')
-rw-r--r--Test/stratifiedinline/Answer454
1 files changed, 227 insertions, 227 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
-----
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 03:00:47 +0000