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