warning: Ignored call to f3/3 in equation f2/3 warning: Ignored call to loop_cont_f1/3 in equation f2/3 Inferred cost of f1(A,B,C,D,E,F,G): f1(A,B,C,D,E,F,G):[9]: 1 with precondition: [A=500,C=499,D=1,E=500,G=499] f1(A,B,C,D,E,F,G):[[8],9]: 1+it1*(1) Such that:it1=<-1*A+500,it1=<-1*C+499,it1=<-1*G+499 with precondition: [D=1,E=500,C=G,499>=A,A>=C+1] Inferred cost of f2(A,B,C): f2(A,B,C):[11]: 1 with precondition: [] f2(A,B,C):[12]: 2 with precondition: [] f2(A,B,C):[13]: inf with precondition: [] Solved cost expressions of f2(A,B,C): f2(A,B,C):[11]: 1 with precondition: [] f2(A,B,C):[12]: 2 with precondition: [] f2(A,B,C):[13]: inf with precondition: [] Maximum cost of f2(A,B,C): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 2 ms. Invariants computed in 9 ms. ----Backward Invariants 3 ms. ----Transitive Invariants 1 ms. Refinement performed in 8 ms. Termination proved in 3 ms. Upper bounds computed in 11 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 6 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 40 ms.