warning: Ignored call to loop_cont_f23/3 in equation loop_cont_f8/3 Inferred cost of f8(A,B,C,D,E,F,G): f8(A,B,C,D,E,F,G):[[15,16],17]: 1+it1*(2)+it2*(1) Such that:it1+it2=<1000,it1+it2=<-1*A+1000 with precondition: [D=0,E=0,F=999,C=G,999>=A,A>=0] Inferred cost of f23(A,B,C,D,E,F,G): f23(A,B,C,D,E,F,G):[21]: 1 with precondition: [D=1,F=B,G=C,A=E,A>=1000] f23(A,B,C,D,E,F,G):[[19,20],21]: 1+it1*(2)+it2*(1) Such that:it1+it2=<-1*A+1000 with precondition: [D=1,E=1000,B=F,999>=A] Inferred cost of loop_cont_f8(A,B,C): loop_cont_f8(A,B,C):[23]: 1 with precondition: [A>=1000] loop_cont_f8(A,B,C):[24]: 1+it1*(2)+it2*(1) Such that:it1+it2=<-1*A+1000 with precondition: [999>=A] Inferred cost of f0(A,B,C): f0(A,B,C):[26]: 3+it1*(2)+it2*(1)+it3*(2)+it4*(1) Such that:it1+it2=<1000,it3+it4=<1000 with precondition: [] Solved cost expressions of f0(A,B,C): f0(A,B,C):[26]: 4003 with precondition: [] Maximum cost of f0(A,B,C): 4003 Asymptotic class: constant Time statistics: Partial evaluation computed in 7 ms. Invariants computed in 17 ms. ----Backward Invariants 7 ms. ----Transitive Invariants 2 ms. Refinement performed in 21 ms. Termination proved in 7 ms. Upper bounds computed in 16 ms. ----Phase cost structures 5 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: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 87 ms.