warning: Ignored call to loop_cont_f10/2 in equation loop_cont_f4/2 Inferred cost of f4(A,B,C,D,E): f4(A,B,C,D,E):[[13],14]: 1+it1*(1) Such that:it1=<2,it1=<-1*A+2 with precondition: [C=0,D=2,E=0,1>=A,A>=0] Inferred cost of f10(A,B,C,D,E): f10(A,B,C,D,E):[17]: 1 with precondition: [C=1,D=A,B=E,B>=2] f10(A,B,C,D,E):[[16],17]: 1+it1*(1) Such that:it1=<-1*B+2 with precondition: [C=1,E=2,A=D,1>=B] Inferred cost of loop_cont_f4(A,B): loop_cont_f4(A,B):[19]: 1 with precondition: [B>=2] loop_cont_f4(A,B):[20]: 1+it1*(1) Such that:it1=<-1*B+2 with precondition: [1>=B] Inferred cost of f0(A,B): f0(A,B):[22]: 3+it1*(1)+it2*(1) Such that:it1=<2,it2=<2 with precondition: [] Solved cost expressions of f0(A,B): f0(A,B):[22]: 7 with precondition: [] Maximum cost of f0(A,B): 7 Asymptotic class: constant Time statistics: Partial evaluation computed in 4 ms. Invariants computed in 12 ms. ----Backward Invariants 5 ms. ----Transitive Invariants 2 ms. Refinement performed in 10 ms. Termination proved in 5 ms. Upper bounds computed in 13 ms. ----Phase cost structures 4 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 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 54 ms.