warning: Ignored call to evalfstop/6 in equation evalfreturnin/6 Inferred cost of evalfbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M): evalfbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M):[22]: 1 with precondition: [G=0,H=A,I=B,C=J,D=K,E=L,E+F=D,E+M=D,0>=2*E+1,C>=E] evalfbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[21],22]: 1+it1*(2) Such that:it1=<2*C+1,it1=<2*E+1,it1=<2*J+1,it1=<2*L+1,it1=<-2*K+2*M+ -1,it1=<-1*K+1*J+1*M,it1=<1*E+1*J+1,it1=<1*C+1*D+ -1*F+1,it1=<1*D+1*J+ -1*F+1,it1=<1*D+1*L+ -1*F+1,it1=<1*J+1*K+ -1*F+1,it1=<1*K+1*L+ -1*F+1 with precondition: [G=0,L=E,A=H,B=I,C=J,D=K,D+L+1=M,C>=L,F+L>=D,D+L>=F] Inferred cost of evalfbb5in(A,B,C,D,E,F,G,H,I,J,K,L,M): evalfbb5in(A,B,C,D,E,F,G,H,I,J,K,L,M):[26]: 1 with precondition: [G=0,B=E,M=F,A=H,B=I,C=J,D=K,B=L,B>=C+1,A>=D] evalfbb5in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[24],[25],26]: 1+it1*(4+it2*(2))+it3*(4) Such that:it1=<1*L,it1=<-1*B+1*J,it1=<-1*D+1*M,it1=<-1*E+1*J,it1=<-1*I+1*J,it1=<-1*K+1*M,it1=<1*C+1,it1=<1*J+1,it1=<1*J+ -1*B,it1=<1*M+ -1*D,it1=<1*M+ -1*K,it1=<1*M+ -1*I+ -1*K+ -1,it3=<-1*B+1,it3=<-1*B+1/2,it3=<-1*E+1,it3=<-1*E+1/2,it3=<-1*I+1,it3=<-1*I+1/2,it3=<-1*B+1*J+1,it3=<-1*B+1*L+ -1,it3=<-1*E+1*L+ -1,it3=<-1*I+1*J+1,it3=<-1*I+1*L+ -1,it3=<1*J+ -1*E+1,it3=<-1*E+ -1*K+1*M+ -1 it2=<2*C+1 with precondition: [G=0,L=C+1,K=D,A=H,B=I,L=J+1,K+L=M,0>=2*E+1,L>=1,E>=B,L>=E+2,A>=K] evalfbb5in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[24],26]: 1+it1*(4) Such that:it1=<-1*B+1,it1=<-1*B+1*L,it1=<-1*E+1,it1=<-1*I+1,it1=<-1*I+1*L,it1=<1*L+ -1*E with precondition: [G=0,L=C+1,K=D,A=H,B=I,L=J+1,L+M=K+1,1>=2*L,E>=B,L>=E+1,A>=K] evalfbb5in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[25],26]: 1+it1*(4+it2*(2)) Such that:it1=<1*L,it1=<-1*I+1*L,it1=<-1*K+1*M,it1=<1*C+1,it1=<1*J+1,it1=<-1*B+ -1*K+1*M,it1=<1*M+ -1*E+ -1*K it2=<2*C+1 with precondition: [G=0,L=C+1,K=D,A=H,B=I,L=J+1,K+L=M,E>=0,E>=B,L>=E+1,A>=K] Inferred cost of evalfbb7in(A,B,C,D,E,F,G,H,I,J,K,L,M): evalfbb7in(A,B,C,D,E,F,G,H,I,J,K,L,M):[32]: 1 with precondition: [G=0,I=B,J=C,L=E,M=F,A=H,D=K,D>=A+1] evalfbb7in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[28],32]: 1+it1*(3) Such that:it1=<1*A+ -1*D+1,it1=<1*H+ -1*D+1 with precondition: [G=0,A=H,B=I,C=J,A+1=K,B=L,F=M,B>=C+1,A>=D] evalfbb7in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[29],32]: 1+it1*(3+it2*(4+it3*(2))+it4*(4)) Such that:it1=<1*A+ -1*D+1,it1=<1*H+ -1*D+1 it4=<1*C+ -1*B+1,it4=<1*C+ -1*B,it4=<-1*B+1/2,it4=<-1*B+1,it2=<1*C+ -1*B,it2=<1*C+1 it3=<2*C+1 with precondition: [G=0,A=H,B=I,C=J,A+1=K,C+1=L,A+C+1=M,0>=2*B+1,C>=0,C>=B+1,A>=D] evalfbb7in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[30],32]: 1+it1*(3+it2*(4)) Such that:it1=<1*A+ -1*D+1,it1=<1*H+ -1*D+1 it2=<1*C+ -1*B+1,it2=<-1*B+1 with precondition: [G=0,A=H,B=I,C=J,A+1=K,C+1=L,A=C+M,0>=2*C+1,C>=B,A>=D] evalfbb7in(A,B,C,D,E,F,G,H,I,J,K,L,M):[[31],32]: 1+it1*(3+it2*(4+it3*(2))) Such that:it1=<1*A+ -1*D+1,it1=<1*H+ -1*D+1 it2=<1*C+ -1*B+1,it2=<1*C+1 it3=<2*C+1 with precondition: [G=0,A=H,B=I,C=J,A+1=K,C+1=L,A+C+1=M,B>=0,C>=B,A>=D] Inferred cost of evalfreturnin(A,B,C,D,E,F): evalfreturnin(A,B,C,D,E,F):[34]: 1 with precondition: [] Inferred cost of loop_cont_evalfbb7in(A,B,C,D,E,F): loop_cont_evalfbb7in(A,B,C,D,E,F):[36]: 1 with precondition: [] Inferred cost of evalfentryin(A,B,C,D,E,F): evalfentryin(A,B,C,D,E,F):[38]: 3 with precondition: [A>=B+1] evalfentryin(A,B,C,D,E,F):[39]: 3+it1*(3) Such that:it1=<1*B+ -1*A+1 with precondition: [B>=A,C>=D+1] evalfentryin(A,B,C,D,E,F):[40]: 3+it1*(3+it2*(4+it3*(2))+it4*(4)) Such that:it1=<1*B+ -1*A+1 it4=<1*D+ -1*C+1,it4=<1*D+ -1*C,it4=<-1*C+1/2,it4=<-1*C+1,it2=<1*D+ -1*C,it2=<1*D+1 it3=<2*D+1 with precondition: [0>=2*C+1,D>=0,B>=A,D>=C+1] evalfentryin(A,B,C,D,E,F):[41]: 3+it1*(3+it2*(4)) Such that:it1=<1*B+ -1*A+1 it2=<1*D+ -1*C+1,it2=<-1*C+1 with precondition: [0>=2*D+1,B>=A,D>=C] evalfentryin(A,B,C,D,E,F):[42]: 3+it1*(3+it2*(4+it3*(2))) Such that:it1=<1*B+ -1*A+1 it2=<1*D+ -1*C+1,it2=<1*D+1 it3=<2*D+1 with precondition: [C>=0,B>=A,D>=C] Inferred cost of evalfstart(A,B,C,D,E,F): evalfstart(A,B,C,D,E,F):[44]: 4 with precondition: [A>=B+1] evalfstart(A,B,C,D,E,F):[45]: 4+it1*(3) Such that:it1=<1*B+ -1*A+1 with precondition: [B>=A,C>=D+1] evalfstart(A,B,C,D,E,F):[46]: 4+it1*(3+it2*(4+it3*(2))+it4*(4)) Such that:it1=<1*B+ -1*A+1 it4=<1*D+ -1*C+1,it4=<1*D+ -1*C,it4=<-1*C+1/2,it4=<-1*C+1,it2=<1*D+ -1*C,it2=<1*D+1 it3=<2*D+1 with precondition: [0>=2*C+1,D>=0,B>=A,D>=C+1] evalfstart(A,B,C,D,E,F):[47]: 4+it1*(3+it2*(4)) Such that:it1=<1*B+ -1*A+1 it2=<1*D+ -1*C+1,it2=<-1*C+1 with precondition: [0>=2*D+1,B>=A,D>=C] evalfstart(A,B,C,D,E,F):[48]: 4+it1*(3+it2*(4+it3*(2))) Such that:it1=<1*B+ -1*A+1 it2=<1*D+ -1*C+1,it2=<1*D+1 it3=<2*D+1 with precondition: [C>=0,B>=A,D>=C] Solved cost expressions of evalfstart(A,B,C,D,E,F): evalfstart(A,B,C,D,E,F):[44]: 4 with precondition: [A>=B+1] evalfstart(A,B,C,D,E,F):[45]: -3*A+3*B+7 with precondition: [B>=A,C>=D+1] evalfstart(A,B,C,D,E,F):[46]: (-1*A+1*B+1)*nat((4*D+6)*nat(min([1*D+1,-1*C+1*D]))+nat(min([-1*C+1/2,-1*C+1*D]))*4+3)+4 with precondition: [0>=2*C+1,D>=0,B>=A,D>=C+1] evalfstart(A,B,C,D,E,F):[47]: (-1*A+1*B+1)* (-4*C+4*D+7)+4 with precondition: [0>=2*D+1,B>=A,D>=C] evalfstart(A,B,C,D,E,F):[48]: (-1*A+1*B+1)*nat((-1*C+1*D+1)* (4*D+6)+3)+4 with precondition: [C>=0,B>=A,D>=C] Maximum cost of evalfstart(A,B,C,D,E,F): max([-3*A+3*B+7,4, (-1*A+1*B+1)*nat((-1*C+1*D+1)* (4*D+6)+3)+4, (-1*A+1*B+1)*nat((4*D+6)*nat(min([1*D+1,-1*C+1*D]))+nat(min([-1*C+1/2,-1*C+1*D]))*4+3)+4, (-1*A+1*B+1)* (-4*C+4*D+7)+4]) Asymptotic class: n^3 Time statistics: Partial evaluation computed in 27 ms. Invariants computed in 132 ms. ----Backward Invariants 62 ms. ----Transitive Invariants 19 ms. Refinement performed in 85 ms. Termination proved in 41 ms. Upper bounds computed in 687 ms. ----Phase cost structures 336 ms. --------Equation cost structures 260 ms. --------Inductive compression(1) 14 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 338 ms. ----Solving cost expressions 5 ms. Compressed phase information: 1 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 1009 ms.