Test/stratifiedinline/bar7.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

(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