warning: Ignored call to loop_cont_f28/4 in equation loop_cont_f19/4 Warning: the following predicates are never called:[f8/4] Inferred cost of f19(A,B,C,D,E,F,G,H,I): f19(A,B,C,D,E,F,G,H,I):[[13],14]: 1+it1*(1) Such that:it1=<1000,it1=<1*B+1 with precondition: [D=1,E=0,G+1=0,H=999,I=1,A=F,999>=B,B>=0] Inferred cost of f28(A,B,C,D,E,F,G,H,I): f28(A,B,C,D,E,F,G,H,I):[17]: 1 with precondition: [E=1,F=A,G=B,I=D,C=H,0>=C+1] f28(A,B,C,D,E,F,G,H,I):[[16],17]: 1+it1*(1) Such that:it1=<1*C+1 with precondition: [E=1,H+1=0,A=F,B=G,D=I,C>=0] Inferred cost of loop_cont_f19(A,B,C,D): loop_cont_f19(A,B,C,D):[19]: 1 with precondition: [0>=C+1] loop_cont_f19(A,B,C,D):[20]: 1+it1*(1) Such that:it1=<1*C+1 with precondition: [C>=0] Inferred cost of f0(A,B,C,D): f0(A,B,C,D):[22]: 3+it1*(1)+it2*(1) Such that:it1=<1000,it2=<1000 with precondition: [] Solved cost expressions of f0(A,B,C,D): f0(A,B,C,D):[22]: 2003 with precondition: [] Maximum cost of f0(A,B,C,D): 2003 Asymptotic class: constant Time statistics: Partial evaluation computed in 6 ms. Invariants computed in 19 ms. ----Backward Invariants 7 ms. ----Transitive Invariants 4 ms. Refinement performed in 18 ms. Termination proved in 7 ms. Upper bounds computed in 17 ms. ----Phase cost structures 5 ms. --------Equation cost structures 3 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 9 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 83 ms.