Test/stratifiedinline/bar10.bpl.expect


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
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