warning: Ignored call to loop_cont_f2/6 in equation f3/6 Inferred cost of f2(A,B,C,D,E,F,G,H,I,J,K,L,M): f2(A,B,C,D,E,F,G,H,I,J,K,L,M):[9]: 1 with precondition: [G=1,H=A,J=C,K=D,L=E,0>=B,0>=I] f2(A,B,C,D,E,F,G,H,I,J,K,L,M):[10]: 1 with precondition: [G=1,J=C,K=D,L=E,A=H,B=I,0>=A,B>=1] f2(A,B,C,D,E,F,G,H,I,J,K,L,M):[[8],9]: 1+it1*(1) Such that:it1=<1*A,it1=<1*B,it1=<1*A+ -1*L+ -1 with precondition: [G=1,K=1,H+1=J,H=L+1,B+H=A,0>=I,H>=0,A>=H+1] f2(A,B,C,D,E,F,G,H,I,J,K,L,M):[[8],10]: 1+it1*(1) Such that:it1=<1*A,it1=<1*B,it1=<1*B+ -1*I with precondition: [G=1,H=0,J=1,L+1=0,A+I=B,A+K=B+1,A>=1,B>=A+1] Inferred cost of f3(A,B,C,D,E,F): f3(A,B,C,D,E,F):[12]: 2 with precondition: [0>=B] f3(A,B,C,D,E,F):[13]: 2 with precondition: [0>=A,B>=1] f3(A,B,C,D,E,F):[14]: 2+it1*(1) Such that:it1=<1*A,it1=<1*B with precondition: [B>=1,A>=B] f3(A,B,C,D,E,F):[15]: 2+it1*(1) Such that:it1=<1*A,it1=<1*B,it1=<1*B+ -1 with precondition: [A>=1,B>=A+1] Solved cost expressions of f3(A,B,C,D,E,F): f3(A,B,C,D,E,F):[12]: 2 with precondition: [0>=B] f3(A,B,C,D,E,F):[13]: 2 with precondition: [0>=A,B>=1] f3(A,B,C,D,E,F):[14]: 1*B+2 with precondition: [B>=1,A>=B] f3(A,B,C,D,E,F):[15]: 1*A+2 with precondition: [A>=1,B>=A+1] Maximum cost of f3(A,B,C,D,E,F): max([1*B+2,2,1*A+2]) Asymptotic class: n Time statistics: Partial evaluation computed in 4 ms. Invariants computed in 23 ms. ----Backward Invariants 14 ms. ----Transitive Invariants 3 ms. Refinement performed in 19 ms. Termination proved in 7 ms. Upper bounds computed in 31 ms. ----Phase cost structures 8 ms. --------Equation cost structures 8 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 96 ms.