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