summaryrefslogtreecommitdiff
path: root/Test/stratifiedinline/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/stratifiedinline/Answer')
-rw-r--r--Test/stratifiedinline/Answer519
1 files changed, 0 insertions, 519 deletions
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
deleted file mode 100644
index 2a3d7605..00000000
--- a/Test/stratifiedinline/Answer
+++ /dev/null
@@ -1,519 +0,0 @@
------ Running regression test bar1.bpl
-(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
------
------ Running regression test bar2.bpl
-(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
------
------ Running regression test bar3.bpl
-(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
------
------ Running regression test bar4.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test bar6.bpl
-
-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(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
------
------ Running regression test bar8.bpl
-(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
------
------ Running regression test bar9.bpl
-(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
------
------ Running regression test bar10.bpl
-(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
------
------ Running regression test bar11.bpl
-(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
------
------ Running regression test bar12.bpl
-(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
------
------ Running regression test bar13.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test large.bpl to test for StackOverflowException
-
-Boogie program verifier finished with 1 verified, 0 errors
------
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 23:38:45 +0000