warning: Ignored call to loop_cont_f300/3 in equation f2/3 Inferred cost of f300(A,B,C,D,E,F,G): f300(A,B,C,D,E,F,G):[9]: 1 with precondition: [D=1,A=E,B=F,0>=A,B>=1] f300(A,B,C,D,E,F,G):[10]: 1 with precondition: [D=1,E=A,B=F,0>=B] f300(A,B,C,D,E,F,G):[[8],10]: 1+it1*(1) Such that:it1=<1*A,it1=<1*A+ -1*F+ -1 with precondition: [D=1,E=F+1,1>=E,A>=1,B>=1,A>=E+1] Inferred cost of f2(A,B,C): f2(A,B,C):[12]: 2 with precondition: [0>=A,B>=1] f2(A,B,C):[13]: 2 with precondition: [0>=B] f2(A,B,C):[14]: 2+it1*(1) Such that:it1=<1*A with precondition: [A>=1,B>=1] Solved cost expressions of f2(A,B,C): f2(A,B,C):[12]: 2 with precondition: [0>=A,B>=1] f2(A,B,C):[13]: 2 with precondition: [0>=B] f2(A,B,C):[14]: 1*A+2 with precondition: [A>=1,B>=1] Maximum cost of f2(A,B,C): max([1*A+2,2]) Asymptotic class: n Time statistics: Partial evaluation computed in 2 ms. Invariants computed in 9 ms. ----Backward Invariants 4 ms. ----Transitive Invariants 2 ms. Refinement performed in 11 ms. Termination proved in 3 ms. Upper bounds computed in 12 ms. ----Phase cost structures 4 ms. --------Equation cost structures 4 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 5 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 45 ms.