warning: Ignored call to f12/1 in equation f0/1 warning: Ignored call to loop_cont_f5/1 in equation f0/1 Inferred cost of f5(A,B,C): f5(A,B,C):[9]: 1 with precondition: [B=1,A=C,A>=20] f5(A,B,C):[[8],9]: 1+it1*(1) Such that:it1=<19,it1=<-1*A+20 with precondition: [B=1,C=20,19>=A,A>=1] Inferred cost of f0(A): f0(A):[11]: 1 with precondition: [] f0(A):[12]: 2 with precondition: [] f0(A):[13]: 2+it1*(1) Such that:it1=<19 with precondition: [] Solved cost expressions of f0(A): f0(A):[11]: 1 with precondition: [] f0(A):[12]: 2 with precondition: [] f0(A):[13]: 21 with precondition: [] Maximum cost of f0(A): 21 Asymptotic class: constant Time statistics: Partial evaluation computed in 1 ms. Invariants computed in 5 ms. ----Backward Invariants 2 ms. ----Transitive Invariants 1 ms. Refinement performed in 5 ms. Termination proved in 1 ms. Upper bounds computed in 7 ms. ----Phase cost structures 1 ms. --------Equation cost structures 1 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 3 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 24 ms.