warning: Ignored call to f14/1 in equation f11/1 warning: Ignored call to f14/1 in equation f11/1 Inferred cost of f4(A,B,C): f4(A,B,C):[15]: 1 with precondition: [A=0,B=0,C=0] f4(A,B,C):[[13],14]: 2+it1*(2) Such that:it1=<3,it1=<-1*A+3 with precondition: [B=0,C=3,2>=A,A>=0] f4(A,B,C):[[13],15]: 1+it1*(2) Such that:it1=<3,it1=<1*C,it1=<-1*A+3,it1=<1*C+ -1*A with precondition: [B=0,3>=C,A>=0,C>=A+1] Inferred cost of f11(A): f11(A):[17]: 1 with precondition: [1>=A] f11(A):[18]: 1 with precondition: [A>=2] Inferred cost of loop_cont_f4(A): loop_cont_f4(A):[20]: 1 with precondition: [1>=A] loop_cont_f4(A):[21]: 1 with precondition: [A>=2] Inferred cost of f0(A): f0(A):[23]: 3 with precondition: [] f0(A):[24]: 4+it1*(2) Such that:it1=<3 with precondition: [] f0(A):[25]: 3+it1*(2) Such that:it1=<1,it1=<3 with precondition: [] f0(A):[26]: 3+it1*(2) Such that:it1=<3 with precondition: [] Solved cost expressions of f0(A): f0(A):[23]: 3 with precondition: [] f0(A):[24]: 10 with precondition: [] f0(A):[25]: 5 with precondition: [] f0(A):[26]: 9 with precondition: [] Maximum cost of f0(A): 10 Asymptotic class: constant Time statistics: Partial evaluation computed in 3 ms. Invariants computed in 8 ms. ----Backward Invariants 3 ms. ----Transitive Invariants 1 ms. Refinement performed in 7 ms. Termination proved in 2 ms. Upper bounds computed in 14 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 7 ms. ----Solving cost expressions 0 ms. Compressed phase information: 1 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 43 ms.