warning: Ignored call to loop_cont_f5/6 in equation f12/6 warning: Ignored call to loop_cont_f5/6 in equation f7/6 warning: Ignored call to loop_cont_f5/6 in equation f8/6 Warning: the following predicates are never called:[f7/6,f8/6] Inferred cost of f5(A,B,C,D,E,F,G,H,I,J,K,L,M): f5(A,B,C,D,E,F,G,H,I,J,K,L,M):[[9],10]: 1+it1*(1) Such that:it1=<400,it1=<-1*B+400 with precondition: [A=400,C=0,G=1,H=400,I=400,J=0,K=0,L=0,M=0,399>=B,B>=0] f5(A,B,C,D,E,F,G,H,I,J,K,L,M):[[9],11]: 1+it1*(1) Such that:it1=<400,it1=<1*I,it1=<-1*B+400,it1=<1*I+ -1*B with precondition: [A=400,C=0,G=1,H=400,M=J,M=K,M=L,400>=I,B>=0,M>=1,I>=B+1] f5(A,B,C,D,E,F,G,H,I,J,K,L,M):[[9],12]: 1+it1*(1) Such that:it1=<400,it1=<1*I,it1=<-1*B+400,it1=<1*I+ -1*B with precondition: [A=400,C=0,G=1,H=400,M=J,M=K,M=L,400>=I,0>=M+1,B>=0,I>=B+1] Inferred cost of f12(A,B,C,D,E,F): f12(A,B,C,D,E,F):[14]: 2+it1*(1) Such that:it1=<400 with precondition: [] f12(A,B,C,D,E,F):[15]: 2+it1*(1) Such that:it1=<400 with precondition: [] f12(A,B,C,D,E,F):[16]: 2+it1*(1) Such that:it1=<400 with precondition: [] Solved cost expressions of f12(A,B,C,D,E,F): f12(A,B,C,D,E,F):[14]: 402 with precondition: [] f12(A,B,C,D,E,F):[15]: 402 with precondition: [] f12(A,B,C,D,E,F):[16]: 402 with precondition: [] Maximum cost of f12(A,B,C,D,E,F): 402 Asymptotic class: constant Time statistics: Partial evaluation computed in 6 ms. Invariants computed in 29 ms. ----Backward Invariants 17 ms. ----Transitive Invariants 3 ms. Refinement performed in 18 ms. Termination proved in 5 ms. Upper bounds computed in 27 ms. ----Phase cost structures 5 ms. --------Equation cost structures 5 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 18 ms. ----Solving cost expressions 1 ms. Compressed phase information: 2 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 100 ms.