warning: Ignored call to loop_cont_f2/1 in equation f3/1 Inferred cost of f2(A,B,C): f2(A,B,C):[10]: 0 with precondition: [B=1,C=A] f2(A,B,C):[[8],[9],10]: inf with precondition: [B=1,0>=C,A>=2] f2(A,B,C):[[8],[9],11]...: inf with precondition: [1>=B,A>=2,B>=0] f2(A,B,C):[[8],10]: 0+it1*(1) Such that:it1=<1*A+ -1,it1=<1*A+ -1*C with precondition: [B=1,C>=1,A>=C+1] f2(A,B,C):[[9],10]: inf with precondition: [B=1,1>=A,A>=C+1] f2(A,B,C):[[9],11]...: inf with precondition: [1>=A,1>=B,B>=0] Inferred cost of f3(A): f3(A):[12]: 1 with precondition: [] f3(A):[13]: inf with precondition: [A>=2] f3(A):[14]: 1+it1*(1) Such that:it1=<1*A+ -1 with precondition: [A>=2] f3(A):[15]: inf with precondition: [1>=A] f3(A):[16]...: inf with precondition: [A>=2] f3(A):[17]...: inf with precondition: [1>=A] f3(A):[18]...: inf with precondition: [A>=2] f3(A):[19]...: inf with precondition: [1>=A] Solved cost expressions of f3(A): f3(A):[12]: 1 with precondition: [] f3(A):[13]: inf with precondition: [A>=2] f3(A):[14]: 1*A with precondition: [A>=2] f3(A):[15]: inf with precondition: [1>=A] f3(A):[16]...: inf with precondition: [A>=2] f3(A):[17]...: inf with precondition: [1>=A] f3(A):[18]...: inf with precondition: [A>=2] f3(A):[19]...: inf with precondition: [1>=A] Maximum cost of f3(A): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 1 ms. Invariants computed in 16 ms. ----Backward Invariants 8 ms. ----Transitive Invariants 1 ms. Refinement performed in 8 ms. Termination proved in 2 ms. Upper bounds computed in 21 ms. ----Phase cost structures 3 ms. --------Equation cost structures 2 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 15 ms. ----Solving cost expressions 0 ms. Compressed phase information: 8 Compressed Chains: 0 Compressed invariants: 2 Total analysis performed in 58 ms.