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):[8]: 1 with precondition: [D=1,A=E,B=F,A>=B] f300(A,B,C,D,E,F,G):[[7],8]: 1+it1*(1) Such that:it1=<1*E+ -1*A,it1=<1*F+ -1*A with precondition: [D=1,B=E,B=F,B>=A+1] Inferred cost of f2(A,B,C): f2(A,B,C):[10]: 2 with precondition: [A>=B] f2(A,B,C):[11]: 2+it1*(1) Such that:it1=<1*B+ -1*A with precondition: [B>=A+1] Solved cost expressions of f2(A,B,C): f2(A,B,C):[10]: 2 with precondition: [A>=B] f2(A,B,C):[11]: -1*A+1*B+2 with precondition: [B>=A+1] Maximum cost of f2(A,B,C): max([-1*A+1*B+2,2]) Asymptotic class: n Time statistics: Partial evaluation computed in 2 ms. Invariants computed in 7 ms. ----Backward Invariants 3 ms. ----Transitive Invariants 1 ms. Refinement performed in 9 ms. Termination proved in 2 ms. Upper bounds computed in 11 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 4 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 37 ms.