warning: Ignored call to loop_cont_f2/3 in equation f0/3 warning: Ignored call to loop_cont_f5/3 in equation loop_cont_f3/3 Inferred cost of f2(A,B,C,D,E,F,G): f2(A,B,C,D,E,F,G):[19]: 0 with precondition: [A=0,D=1,E=0,F=B,C=G,C>=1] f2(A,B,C,D,E,F,G):[[18],19]: inf with precondition: [D=1,B=F,C=G,A>=0,C>=1,E>=A+1] f2(A,B,C,D,E,F,G):[[18],20]...: inf with precondition: [1>=D,A>=0,C>=1,D>=0] Inferred cost of f3(A,B,C,D,E,F,G): f3(A,B,C,D,E,F,G):[22]: 1 with precondition: [A=0,D=0,E=0,B=F,C=G,0>=B,0>=C] f3(A,B,C,D,E,F,G):[[21],22]: 1+it1*(1) Such that:it1=<1*B with precondition: [A=0,D=0,E=0,F=0,C=G,0>=C,B>=1] Inferred cost of f5(A,B,C,D,E,F,G): f5(A,B,C,D,E,F,G):[25]: 0 with precondition: [D=1,E=A,F=B,G=C] f5(A,B,C,D,E,F,G):[[24],25]: inf with precondition: [D=1,G=1,A=E,B=F] f5(A,B,C,D,E,F,G):[[24],26]...: inf with precondition: [1>=D,D>=0] Inferred cost of loop_cont_f3(A,B,C): loop_cont_f3(A,B,C):[27]: 0 with precondition: [] loop_cont_f3(A,B,C):[28]: inf with precondition: [] loop_cont_f3(A,B,C):[29]...: inf with precondition: [] loop_cont_f3(A,B,C):[30]...: inf with precondition: [] Inferred cost of f0(A,B,C): f0(A,B,C):[32]: 2 with precondition: [0>=B,0>=C] f0(A,B,C):[33]: inf with precondition: [0>=B,0>=C] f0(A,B,C):[34]: 2+it1*(1) Such that:it1=<1*B with precondition: [0>=C,B>=1] f0(A,B,C):[35]: inf with precondition: [0>=C,B>=1] f0(A,B,C):[36]: 1 with precondition: [C>=1] f0(A,B,C):[37]: inf with precondition: [C>=1] f0(A,B,C):[38]...: inf with precondition: [0>=B,0>=C] f0(A,B,C):[39]...: inf with precondition: [0>=B,0>=C] f0(A,B,C):[40]...: inf with precondition: [0>=C,B>=1] f0(A,B,C):[41]...: inf with precondition: [0>=C,B>=1] f0(A,B,C):[42]...: inf with precondition: [C>=1] f0(A,B,C):[43]...: inf with precondition: [C>=1] Solved cost expressions of f0(A,B,C): f0(A,B,C):[32]: 2 with precondition: [0>=B,0>=C] f0(A,B,C):[33]: inf with precondition: [0>=B,0>=C] f0(A,B,C):[34]: 1*B+2 with precondition: [0>=C,B>=1] f0(A,B,C):[35]: inf with precondition: [0>=C,B>=1] f0(A,B,C):[36]: 1 with precondition: [C>=1] f0(A,B,C):[37]: inf with precondition: [C>=1] f0(A,B,C):[38]...: inf with precondition: [0>=B,0>=C] f0(A,B,C):[39]...: inf with precondition: [0>=B,0>=C] f0(A,B,C):[40]...: inf with precondition: [0>=C,B>=1] f0(A,B,C):[41]...: inf with precondition: [0>=C,B>=1] f0(A,B,C):[42]...: inf with precondition: [C>=1] f0(A,B,C):[43]...: inf with precondition: [C>=1] Maximum cost of f0(A,B,C): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 6 ms. Invariants computed in 30 ms. ----Backward Invariants 17 ms. ----Transitive Invariants 3 ms. Refinement performed in 29 ms. Termination proved in 7 ms. Upper bounds computed in 30 ms. ----Phase cost structures 11 ms. --------Equation cost structures 11 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 16 ms. ----Solving cost expressions 1 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 118 ms.