Test/stratifiedinline/bar9.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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
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