warning: Ignored call to loop_cont_f1/1 in equation f0/1 Inferred cost of f1(A,B,C): f1(A,B,C):[8]: 0 with precondition: [B=1,C=A] f1(A,B,C):[[7],8]: 0+it1*(1) Such that:it1=<1/1000*A+ -1,it1=<1/1000*A+ -1/1000*C with precondition: [B=1,C>=1,A>=C+1000] Inferred cost of f0(A): f0(A):[10]: 1 with precondition: [] f0(A):[11]: 1+it1*(1) Such that:it1=<1/1000*A+ -1,it1=<1/1000*A+ -1/1000 with precondition: [A>=1001] Solved cost expressions of f0(A): f0(A):[10]: 1 with precondition: [] f0(A):[11]: 1/1000*A with precondition: [A>=1001] Maximum cost of f0(A): max([1/1000*A,1]) Asymptotic class: n Time statistics: Partial evaluation computed in 1 ms. Invariants computed in 4 ms. ----Backward Invariants 1 ms. ----Transitive Invariants 1 ms. Refinement performed in 4 ms. Termination proved in 2 ms. Upper bounds computed in 7 ms. ----Phase cost structures 3 ms. --------Equation cost structures 3 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.