warning: Ignored call to evalNestedLoopstop/8 in equation evalNestedLoopreturnin/8 Inferred cost of evalNestedLoopbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): evalNestedLoopbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[24]: 2 with precondition: [I=0,J=A,M=D,H=F,E+1=G,B=K,C=L,E+1=N,H=O,E+1=P,H=Q,B>=E+1,C>=H+1] evalNestedLoopbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[25]: 1 with precondition: [I=0,J=A,M=D,H=F,E+1=G,B=K,C=L,E+1=N,H=O,E+1=P,H=Q,H>=C,B>=E+1] evalNestedLoopbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[23],24]: 2+it1*(3) Such that:it1=<-1*F+1*L,it1=<-1*F+1*Q,it1=<1*C+ -1*H,it1=<1*L+ -1*H,it1=<1*Q+ -1*H with precondition: [I=0,P=E+1,P=G,A=J,B=K,C=L,D=M,P=N,Q=O,H>=F,Q>=H+1,B>=P,C>=Q+1] evalNestedLoopbb3in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[23],25]: 1+it1*(3) Such that:it1=<-1*F+1*Q,it1=<1*C+ -1*H,it1=<1*Q+ -1*H with precondition: [I=0,P=E+1,P=G,A=J,B=K,C=L,D=M,P=N,C=O,C=Q,H>=F,C>=H+1,B>=P] Inferred cost of evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[31]: 2 with precondition: [E=0,I=0,N=0,L=C,D=F,P=G,Q=H,A=J,B=K,D=M,D=O,B>=1,A>=D+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[32]: 1 with precondition: [E=0,I=0,N=0,L=C,D=F,P=G,Q=H,A=J,B=K,D=M,D=O,0>=B,A>=D+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[28],31]: 2+it1*(4) Such that:it1=<1*K,it1=<1*N,it1=<1*P,it1=<1*B+ -1,it1=<1*B+ -1*E,it1=<1*K+ -1,it1=<1*K+ -1*E,it1=<1*P+ -1*E with precondition: [I=0,O=D,O=F,A=J,B=K,C=L,O=M,N=P,O=Q,E>=0,O>=C,N>=E+1,B>=N+1,A>=O+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[28],32]: 1+it1*(4) Such that:it1=<1*K,it1=<1*N,it1=<1*P,it1=<1*B+ -1*E,it1=<1*P+ -1*E with precondition: [I=0,N=B,O=D,O=F,A=J,N=K,C=L,O=M,N=P,O=Q,E>=0,O>=C,N>=E+1,A>=O+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],30,[28],31]: 6+it1*(4)+it2*(3)+it3*(5)+it4*(3) Such that:it1=<1*B+ -3,it1=<1*B+ -2,it1=<1*K+ -3,it1=<1*K+ -2,it1=<1*N+ -2,it1=<1*P+ -2,it1+it3=<1*B+ -2,it1+it3=<1*K+ -2,it1+it3=<1*K+ -1,it1+it3=<1*N+ -1,it1+it3=<1*P+ -1,it1+it3=<1*B+ -1*E+ -1,it1+it3=<1*K+ -1*E+ -1,it1+it3=<1*P+ -1*E+ -1,it2=<-1*D+1*Q,it2=<-1*M+1*Q,it2=<1*Q+ -1*D,it2=<1*Q+ -1*F,it2=<1*Q+ -1*M,it2+it4=<-1*D+1*Q,it2+it4=<-1*M+1*Q,it2+it4=<1*Q+ -1*F,it3=<1*K,it3=<1*B+ -1*E,it3=<1*K+ -1*E,it4=<-1*D+1*Q+ -1,it4=<-1*M+1*Q+ -1,it4=<1*Q+ -1*F+ -1 with precondition: [I=0,O=C,M=D,A=J,B=K,O=L,N=P,O=Q,E>=0,N>=E+3,O>=F+1,A>=M+1,F>=M,B>=N+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],30,[28],32]: 5+it1*(4)+it2*(3)+it3*(5)+it4*(3) Such that:it1=<1*B+ -2,it1=<1*K+ -2,it1=<1*N+ -2,it1=<1*P+ -2,it1+it3=<1*K+ -1,it1+it3=<1*N+ -1,it1+it3=<1*P+ -1,it1+it3=<1*B+ -1*E+ -1,it1+it3=<1*P+ -1*E+ -1,it2=<-1*D+1*Q,it2=<-1*M+1*Q,it2=<1*Q+ -1*D,it2=<1*Q+ -1*F,it2=<1*Q+ -1*M,it2+it4=<-1*D+1*Q,it2+it4=<-1*M+1*Q,it2+it4=<1*Q+ -1*F,it3=<1*K,it3=<1*N,it3=<1*P,it3=<1*B+ -1*E,it3=<1*P+ -1*E,it4=<-1*D+1*Q+ -1,it4=<-1*M+1*Q+ -1,it4=<1*Q+ -1*F+ -1 with precondition: [I=0,O=C,M=D,A=J,B=K,O=L,B=N,B=P,O=Q,E>=0,B>=E+3,O>=F+1,A>=M+1,F>=M] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],30,31]: 6+it1*(3)+it2*(5)+it3*(3) Such that:it1=<-1*D+1*Q,it1=<-1*M+1*Q,it1=<1*Q+ -1*D,it1=<1*Q+ -1*F,it1=<1*Q+ -1*M,it1+it3=<-1*D+1*Q,it1+it3=<-1*M+1*Q,it1+it3=<1*Q+ -1*F,it2=<1*K,it2=<1*B+ -2,it2=<1*B+ -1*E,it2=<1*K+ -2,it2=<1*K+ -1*E,it2=<1*N+ -1,it2=<1*P+ -1,it2=<1*P+ -1*E+ -1,it3=<-1*D+1*Q+ -1,it3=<-1*M+1*Q+ -1,it3=<1*Q+ -1*F+ -1 with precondition: [I=0,O=C,M=D,A=J,B=K,O=L,N=P,O=Q,E>=0,N>=E+2,O>=F+1,A>=M+1,F>=M,B>=N+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],30,32]: 5+it1*(3)+it2*(5)+it3*(3) Such that:it1=<-1*D+1*Q,it1=<-1*M+1*Q,it1=<1*Q+ -1*D,it1=<1*Q+ -1*F,it1=<1*Q+ -1*M,it1+it3=<-1*D+1*Q,it1+it3=<-1*M+1*Q,it1+it3=<1*Q+ -1*F,it2=<1*K,it2=<1*N,it2=<1*P,it2=<1*B+ -1*E,it2=<1*K+ -1,it2=<1*N+ -1,it2=<1*P+ -1,it2=<1*P+ -1*E,it2=<1*B+ -1*E+ -1,it2=<1*P+ -1*E+ -1,it3=<-1*D+1*Q+ -1,it3=<-1*M+1*Q+ -1,it3=<1*Q+ -1*F+ -1 with precondition: [I=0,O=C,M=D,A=J,B=K,O=L,B=N,B=P,O=Q,E>=0,B>=E+2,O>=F+1,A>=M+1,F>=M] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],31]: 2+it1*(5)+it2*(3) Such that:it1=<1*K,it1=<1*N,it1=<1*P,it1=<1*B+ -1,it1=<1*B+ -1*E,it1=<1*K+ -1,it1=<1*K+ -1*E,it1=<1*P+ -1*E,it2=<-1*D+1*Q,it2=<-1*M+1*Q,it2=<1*Q+ -1*F,it2=<-1*D+1*C+ -1,it2=<-1*M+1*L+ -1,it2=<1*L+ -1*F+ -1 with precondition: [I=0,M=D,A=J,B=K,C=L,N=P,O=Q,E>=0,N>=E+1,O>=F,A>=M+1,F>=M,B>=N+1,C>=O+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[27,29],32]: 1+it1*(5)+it2*(3) Such that:it1=<1*K,it1=<1*N,it1=<1*P,it1=<1*B+ -1*E,it1=<1*P+ -1*E,it2=<-1*D+1*Q,it2=<-1*M+1*Q,it2=<1*Q+ -1*F,it2=<-1*D+1*C+ -1,it2=<-1*M+1*L+ -1,it2=<1*L+ -1*F+ -1 with precondition: [I=0,N=B,M=D,A=J,N=K,C=L,N=P,O=Q,E>=0,N>=E+1,O>=F,A>=M+1,F>=M,C>=O+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[30,[28],31]: 6+it1*(4)+it2*(3) Such that:it1=<1*B+ -2,it1=<1*B+ -1,it1=<1*K+ -2,it1=<1*K+ -1,it1=<1*N+ -1,it1=<1*P+ -1,it2=<1*Q+ -1*D,it2=<1*Q+ -1*F,it2=<1*Q+ -1*M with precondition: [E=0,I=0,D=F,A=J,B=K,C=L,D=M,C=O,N=P,C=Q,N>=2,A>=D+1,C>=D+1,B>=N+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[30,[28],32]: 5+it1*(4)+it2*(3) Such that:it1=<1*B+ -1,it1=<1*K+ -1,it1=<1*N+ -1,it1=<1*P+ -1,it2=<1*Q+ -1*D,it2=<1*Q+ -1*F,it2=<1*Q+ -1*M with precondition: [E=0,I=0,D=F,A=J,B=K,C=L,D=M,B=N,C=O,B=P,C=Q,B>=2,A>=D+1,C>=D+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[30,31]: 6+it1*(3) Such that:it1=<1*Q+ -1*D,it1=<1*Q+ -1*F,it1=<1*Q+ -1*M with precondition: [E=0,I=0,N=1,P=1,D=F,A=J,B=K,C=L,D=M,C=O,C=Q,B>=2,A>=D+1,C>=D+1] evalNestedLoopbb6in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[30,32]: 5+it1*(3) Such that:it1=<1*Q+ -1*D,it1=<1*Q+ -1*F,it1=<1*Q+ -1*M with precondition: [B=1,E=0,I=0,K=1,N=1,P=1,D=F,A=J,C=L,D=M,C=O,C=Q,A>=D+1,C>=D+1] Inferred cost of evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q): evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[48]: 2 with precondition: [D=0,I=0,M=0,N=E,O=F,P=G,Q=H,A=J,B=K,C=L,A>=1,B>=0,C>=0] evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[49]: 1 with precondition: [A=0,D=0,I=0,J=0,M=0,N=E,O=F,P=G,Q=H,B=K,C=L,B>=0,C>=0] evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[35],48]: 2+it1*(4) Such that:it1=<1*J,it1=<1*M,it1=<1*A+ -1,it1=<1*A+ -1*D,it1=<1*J+ -1,it1=<1*J+ -1*D,it1=<1*O+1,it1=<1*O+ -1*D+1 with precondition: [B=0,I=0,K=0,N=0,A=J,C=L,M=O+1,G=P,H=Q,C>=0,D>=0,M>=D+1,A>=M+1] evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[35],49]: 1+it1*(4) Such that:it1=<1*J,it1=<1*M,it1=<1*A+ -1*D,it1=<1*M+ -1*D,it1=<1*O+1 with precondition: [B=0,I=0,K=0,N=0,A=J,C=L,A=M,A=O+1,G=P,H=Q,C>=0,D>=0,A>=D+1] evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[34,36,37,38,39,40,41,42,43,44,45,46,47],48]: 2+it1*(5)+it2*(5+it3*(4))+it4*(4+it5*(4))+it6*(9+it7*(4)+it8*(3)+it9*(5)+it10*(3))+it11*(8+it12*(4)+it13*(3)+it14*(5)+it15*(3))+it16*(9+it17*(3)+it18*(5)+it19*(3))+it20*(8+it21*(3)+it22*(5)+it23*(3))+it24*(5+it25*(5))+it26*(4+it27*(5))+it28*(3)+it29*(9+it30*(4)+it31*(3))+it32*(8+it33*(4)+it34*(3))+it35*(9+it36*(3))+it37*(8+it38*(3)) Such that:it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*J,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*M,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+ -1,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+ -1*D,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*J+ -1,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*J+ -1*D,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*M+ -1*D,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*O+1,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*J,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*L,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*M,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+ -1/2,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*J+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*J+ -1/2,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*L+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*M+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*O+1/2,it24+it26=<1*C,it24+it26=<1*L,it24+it26=<1*M,it24+it26=<1*A+ -1,it24+it26=<1*J+ -1,it24+it26=<1*L+ -1*D,it24+it26=<1*M+ -1*D,it24+it26=<1*O+1,it28=<1*O,it28=<1*A+ -2,it28=<1*C+ -1,it28=<1*J+ -2,it28=<1*L+ -1,it28=<1*M+ -1,it28=<1*L+ -1*D+ -1,it28=<1*M+ -1*D+ -1 it3=<1*B+ -1,it3=<1*B it5=<1*B it10=<-1*D+1*C+ -1,it10=<1*C+ -1,it9=<1*B,it8+it10=<-1*D+1*C,it8+it10=<1*C,it8=<-1*D+1*C,it8=<1*C,it7+it9=<1*B+ -1,it7+it9=<1*B+ -2,it7=<1*B+ -2,it7=<1*B+ -3 it15=<-1*D+1*C+ -1,it15=<1*C+ -1,it14=<1*B,it13+it15=<-1*D+1*C,it13+it15=<1*C,it13=<-1*D+1*C,it13=<1*C,it12+it14=<1*B+ -1,it12=<1*B+ -2 it19=<-1*D+1*C+ -1,it19=<1*C+ -1,it18=<1*B+ -2,it18=<1*B,it17+it19=<-1*D+1*C,it17+it19=<1*C,it17=<-1*D+1*C,it17=<1*C it23=<-1*D+1*C+ -1,it23=<1*C+ -1,it22=<1*B+ -1,it22=<1*B,it21+it23=<-1*D+1*C,it21+it23=<1*C,it21=<-1*D+1*C,it21=<1*C it25=<1*B+ -1,it25=<1*B it27=<1*B it31=<-1*D+1*C,it31=<1*C,it30=<1*B+ -1,it30=<1*B+ -2 it34=<-1*D+1*C,it34=<1*C,it33=<1*B+ -1 it36=<-1*D+1*C,it36=<1*C it38=<-1*D+1*C,it38=<1*C with precondition: [I=0,A=J,B=K,C=L,O+1=M,B>=1,C>=0,D>=0,N>=0,O>=D,B>=N,A>=O+2] evalNestedLoopbb9in(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q):[[34,36,37,38,39,40,41,42,43,44,45,46,47],49]: 1+it1*(5)+it2*(5+it3*(4))+it4*(4+it5*(4))+it6*(9+it7*(4)+it8*(3)+it9*(5)+it10*(3))+it11*(8+it12*(4)+it13*(3)+it14*(5)+it15*(3))+it16*(9+it17*(3)+it18*(5)+it19*(3))+it20*(8+it21*(3)+it22*(5)+it23*(3))+it24*(5+it25*(5))+it26*(4+it27*(5))+it28*(3)+it29*(9+it30*(4)+it31*(3))+it32*(8+it33*(4)+it34*(3))+it35*(9+it36*(3))+it37*(8+it38*(3)) Such that:it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*J,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*M,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+ -1*D,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+1*C,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*C+1*J,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*J+ -1*D,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*J+1*L,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*M+ -1*D,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*O+1,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*J,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*L,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*M,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C+1/2*J,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*J+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*J+1/2*L,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*L+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*M+ -1/2*D,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*O+1/2,it24+it26=<1*C,it24+it26=<1*L,it24+it26=<1*M,it24+it26=<1*A+1*C,it24+it26=<1*C+1*J,it24+it26=<1*J+1*L,it24+it26=<1*L+ -1*D,it24+it26=<1*M+ -1*D,it24+it26=<1*O+1,it28=<1*O,it28=<1*C+ -1,it28=<1*L+ -1,it28=<1*M+ -1,it28=<1*A+1*C+ -1,it28=<1*J+1*L+ -1,it28=<1*L+ -1*D+ -1,it28=<1*M+ -1*D+ -1 it3=<1*B+ -1,it3=<1*B it5=<1*B it10=<-1*D+1*C+ -1,it10=<1*C+ -1,it9=<1*B,it8+it10=<-1*D+1*C,it8+it10=<1*C,it8=<-1*D+1*C,it8=<1*C,it7+it9=<1*B+ -1,it7+it9=<1*B+ -2,it7=<1*B+ -2,it7=<1*B+ -3 it15=<-1*D+1*C+ -1,it15=<1*C+ -1,it14=<1*B,it13+it15=<-1*D+1*C,it13+it15=<1*C,it13=<-1*D+1*C,it13=<1*C,it12+it14=<1*B+ -1,it12=<1*B+ -2 it19=<-1*D+1*C+ -1,it19=<1*C+ -1,it18=<1*B+ -2,it18=<1*B,it17+it19=<-1*D+1*C,it17+it19=<1*C,it17=<-1*D+1*C,it17=<1*C it23=<-1*D+1*C+ -1,it23=<1*C+ -1,it22=<1*B+ -1,it22=<1*B,it21+it23=<-1*D+1*C,it21+it23=<1*C,it21=<-1*D+1*C,it21=<1*C it25=<1*B+ -1,it25=<1*B it27=<1*B it31=<-1*D+1*C,it31=<1*C,it30=<1*B+ -1,it30=<1*B+ -2 it34=<-1*D+1*C,it34=<1*C,it33=<1*B+ -1 it36=<-1*D+1*C,it36=<1*C it38=<-1*D+1*C,it38=<1*C with precondition: [I=0,A=J,B=K,C=L,M=O+1,B>=1,D>=0,N>=0,M>=A,A>=D+1,B>=N,A+C>=M] Inferred cost of evalNestedLoopreturnin(A,B,C,D,E,F,G,H): evalNestedLoopreturnin(A,B,C,D,E,F,G,H):[51]: 1 with precondition: [] Inferred cost of loop_cont_evalNestedLoopbb9in(A,B,C,D,E,F,G,H): loop_cont_evalNestedLoopbb9in(A,B,C,D,E,F,G,H):[53]: 1 with precondition: [] Inferred cost of evalNestedLoopentryin(A,B,C,D,E,F,G,H): evalNestedLoopentryin(A,B,C,D,E,F,G,H):[55]: 4 with precondition: [A>=1,B>=0,C>=0] evalNestedLoopentryin(A,B,C,D,E,F,G,H):[56]: 3 with precondition: [A=0,B>=0,C>=0] evalNestedLoopentryin(A,B,C,D,E,F,G,H):[57]: 4+it1*(4) Such that:it1=<1*A,it1=<1*A+ -1 with precondition: [B=0,A>=2,C>=0] evalNestedLoopentryin(A,B,C,D,E,F,G,H):[58]: 3+it1*(4) Such that:it1=<1*A with precondition: [B=0,A>=1,C>=0] evalNestedLoopentryin(A,B,C,D,E,F,G,H):[59]: 4+it1*(5)+it2*(5+it3*(4))+it4*(4+it5*(4))+it6*(9+it7*(4)+it8*(3)+it9*(5)+it10*(3))+it11*(8+it12*(4)+it13*(3)+it14*(5)+it15*(3))+it16*(9+it17*(3)+it18*(5)+it19*(3))+it20*(8+it21*(3)+it22*(5)+it23*(3))+it24*(5+it25*(5))+it26*(4+it27*(5))+it28*(3)+it29*(9+it30*(4)+it31*(3))+it32*(8+it33*(4)+it34*(3))+it35*(9+it36*(3))+it37*(8+it38*(3)) Such that:it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+ -1,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+ -1/2,it24+it26=<1*C,it24+it26=<1*A+ -1,it28=<1*A+ -2,it28=<1*C+ -1 it3=<1*B+ -1,it3=<1*B it5=<1*B it10=<1*C+ -1,it9=<1*B,it8+it10=<1*C,it8=<1*C,it7+it9=<1*B+ -1,it7+it9=<1*B+ -2,it7=<1*B+ -2,it7=<1*B+ -3 it15=<1*C+ -1,it14=<1*B,it13+it15=<1*C,it13=<1*C,it12+it14=<1*B+ -1,it12=<1*B+ -2 it19=<1*C+ -1,it18=<1*B+ -2,it18=<1*B,it17+it19=<1*C,it17=<1*C it23=<1*C+ -1,it22=<1*B+ -1,it22=<1*B,it21+it23=<1*C,it21=<1*C it25=<1*B+ -1,it25=<1*B it27=<1*B it31=<1*C,it30=<1*B+ -1,it30=<1*B+ -2 it34=<1*C,it33=<1*B+ -1 it36=<1*C it38=<1*C with precondition: [A>=2,B>=1,C>=0] evalNestedLoopentryin(A,B,C,D,E,F,G,H):[60]: 3+it1*(5)+it2*(5+it3*(4))+it4*(4+it5*(4))+it6*(9+it7*(4)+it8*(3)+it9*(5)+it10*(3))+it11*(8+it12*(4)+it13*(3)+it14*(5)+it15*(3))+it16*(9+it17*(3)+it18*(5)+it19*(3))+it20*(8+it21*(3)+it22*(5)+it23*(3))+it24*(5+it25*(5))+it26*(4+it27*(5))+it28*(3)+it29*(9+it30*(4)+it31*(3))+it32*(8+it33*(4)+it34*(3))+it35*(9+it36*(3))+it37*(8+it38*(3)) Such that:it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+1*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+1/2*C,it24+it26=<1*C,it24+it26=<1*A+1*C,it28=<1*C+ -1,it28=<1*A+1*C+ -1 it3=<1*B+ -1,it3=<1*B it5=<1*B it10=<1*C+ -1,it9=<1*B,it8+it10=<1*C,it8=<1*C,it7+it9=<1*B+ -1,it7+it9=<1*B+ -2,it7=<1*B+ -2,it7=<1*B+ -3 it15=<1*C+ -1,it14=<1*B,it13+it15=<1*C,it13=<1*C,it12+it14=<1*B+ -1,it12=<1*B+ -2 it19=<1*C+ -1,it18=<1*B+ -2,it18=<1*B,it17+it19=<1*C,it17=<1*C it23=<1*C+ -1,it22=<1*B+ -1,it22=<1*B,it21+it23=<1*C,it21=<1*C it25=<1*B+ -1,it25=<1*B it27=<1*B it31=<1*C,it30=<1*B+ -1,it30=<1*B+ -2 it34=<1*C,it33=<1*B+ -1 it36=<1*C it38=<1*C with precondition: [A>=1,B>=1,C>=0] Inferred cost of evalNestedLoopstart(A,B,C,D,E,F,G,H): evalNestedLoopstart(A,B,C,D,E,F,G,H):[62]: 5 with precondition: [A>=1,B>=0,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[63]: 4 with precondition: [A=0,B>=0,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[64]: 5+it1*(4) Such that:it1=<1*A,it1=<1*A+ -1 with precondition: [B=0,A>=2,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[65]: 4+it1*(4) Such that:it1=<1*A with precondition: [B=0,A>=1,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[66]: 5+it1*(5)+it2*(5+it3*(4))+it4*(4+it5*(4))+it6*(9+it7*(4)+it8*(3)+it9*(5)+it10*(3))+it11*(8+it12*(4)+it13*(3)+it14*(5)+it15*(3))+it16*(9+it17*(3)+it18*(5)+it19*(3))+it20*(8+it21*(3)+it22*(5)+it23*(3))+it24*(5+it25*(5))+it26*(4+it27*(5))+it28*(3)+it29*(9+it30*(4)+it31*(3))+it32*(8+it33*(4)+it34*(3))+it35*(9+it36*(3))+it37*(8+it38*(3)) Such that:it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+ -1,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+ -1/2,it24+it26=<1*C,it24+it26=<1*A+ -1,it28=<1*A+ -2,it28=<1*C+ -1 it3=<1*B+ -1,it3=<1*B it5=<1*B it10=<1*C+ -1,it9=<1*B,it8+it10=<1*C,it8=<1*C,it7+it9=<1*B+ -1,it7+it9=<1*B+ -2,it7=<1*B+ -2,it7=<1*B+ -3 it15=<1*C+ -1,it14=<1*B,it13+it15=<1*C,it13=<1*C,it12+it14=<1*B+ -1,it12=<1*B+ -2 it19=<1*C+ -1,it18=<1*B+ -2,it18=<1*B,it17+it19=<1*C,it17=<1*C it23=<1*C+ -1,it22=<1*B+ -1,it22=<1*B,it21+it23=<1*C,it21=<1*C it25=<1*B+ -1,it25=<1*B it27=<1*B it31=<1*C,it30=<1*B+ -1,it30=<1*B+ -2 it34=<1*C,it33=<1*B+ -1 it36=<1*C it38=<1*C with precondition: [A>=2,B>=1,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[67]: 4+it1*(5)+it2*(5+it3*(4))+it4*(4+it5*(4))+it6*(9+it7*(4)+it8*(3)+it9*(5)+it10*(3))+it11*(8+it12*(4)+it13*(3)+it14*(5)+it15*(3))+it16*(9+it17*(3)+it18*(5)+it19*(3))+it20*(8+it21*(3)+it22*(5)+it23*(3))+it24*(5+it25*(5))+it26*(4+it27*(5))+it28*(3)+it29*(9+it30*(4)+it31*(3))+it32*(8+it33*(4)+it34*(3))+it35*(9+it36*(3))+it37*(8+it38*(3)) Such that:it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A,it1+it2+it4+it6+it11+it16+it20+it24+it26+it29+it32+it35+it37=<1*A+1*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*C,it6+it11+it16+it20+it29+it32+it35+it37=<1/2*A+1/2*C,it24+it26=<1*C,it24+it26=<1*A+1*C,it28=<1*C+ -1,it28=<1*A+1*C+ -1 it3=<1*B+ -1,it3=<1*B it5=<1*B it10=<1*C+ -1,it9=<1*B,it8+it10=<1*C,it8=<1*C,it7+it9=<1*B+ -1,it7+it9=<1*B+ -2,it7=<1*B+ -2,it7=<1*B+ -3 it15=<1*C+ -1,it14=<1*B,it13+it15=<1*C,it13=<1*C,it12+it14=<1*B+ -1,it12=<1*B+ -2 it19=<1*C+ -1,it18=<1*B+ -2,it18=<1*B,it17+it19=<1*C,it17=<1*C it23=<1*C+ -1,it22=<1*B+ -1,it22=<1*B,it21+it23=<1*C,it21=<1*C it25=<1*B+ -1,it25=<1*B it27=<1*B it31=<1*C,it30=<1*B+ -1,it30=<1*B+ -2 it34=<1*C,it33=<1*B+ -1 it36=<1*C it38=<1*C with precondition: [A>=1,B>=1,C>=0] Solved cost expressions of evalNestedLoopstart(A,B,C,D,E,F,G,H): evalNestedLoopstart(A,B,C,D,E,F,G,H):[62]: 5 with precondition: [A>=1,B>=0,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[63]: 4 with precondition: [A=0,B>=0,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[64]: 4*A+1 with precondition: [B=0,A>=2,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[65]: 4*A+4 with precondition: [B=0,A>=1,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[66]: nat(min([1*C+ -1,1*A+ -2]))*3+max([5*A+ -5, (1*A+ -1)*nat(3*C+max([nat(1*B+ -2)*4,nat(1*B+ -2)*5])+9), (1*A+ -1)*nat(nat(1*B+ -2)*4+3*C+9), (1*A+ -1)*nat(nat(1*B+ -2)*5+3*C+9), (1*A+ -1)* (5*B), (3*C+8)* (1*A+ -1), (3*C+9)* (1*A+ -1), (4*B+1)* (1*A+ -1), (4*B+4)* (1*A+ -1), (5*B+4)* (1*A+ -1), (4*B+3*C+4)* (1*A+ -1), (5*B+3*C+3)* (1*A+ -1)])+5 with precondition: [A>=2,B>=1,C>=0] evalNestedLoopstart(A,B,C,D,E,F,G,H):[67]: nat(1*C+ -1)*3+max([5*A,1*A*nat(3*C+max([nat(1*B+ -2)*4,nat(1*B+ -2)*5])+9),1*A*nat(nat(1*B+ -2)*4+3*C+9),1*A*nat(nat(1*B+ -2)*5+3*C+9),5*B* (1*A), (3*C+8)* (1*A), (3*C+9)* (1*A), (4*B+1)* (1*A), (4*B+4)* (1*A), (5*B+4)* (1*A), (4*B+3*C+4)* (1*A), (5*B+3*C+3)* (1*A)])+4 with precondition: [A>=1,B>=1,C>=0] Maximum cost of evalNestedLoopstart(A,B,C,D,E,F,G,H): max([4*A+4,5,nat(min([1*C+ -1,1*A+ -2]))*3+max([5*A+ -5, (1*A+ -1)*nat(3*C+max([nat(1*B+ -2)*4,nat(1*B+ -2)*5])+9), (1*A+ -1)*nat(nat(1*B+ -2)*4+3*C+9), (1*A+ -1)*nat(nat(1*B+ -2)*5+3*C+9), (1*A+ -1)* (5*B), (3*C+8)* (1*A+ -1), (3*C+9)* (1*A+ -1), (4*B+1)* (1*A+ -1), (4*B+4)* (1*A+ -1), (5*B+4)* (1*A+ -1), (4*B+3*C+4)* (1*A+ -1), (5*B+3*C+3)* (1*A+ -1)])+5,nat(1*C+ -1)*3+max([5*A,1*A*nat(3*C+max([nat(1*B+ -2)*4,nat(1*B+ -2)*5])+9),1*A*nat(nat(1*B+ -2)*4+3*C+9),1*A*nat(nat(1*B+ -2)*5+3*C+9),5*B* (1*A), (3*C+8)* (1*A), (3*C+9)* (1*A), (4*B+1)* (1*A), (4*B+4)* (1*A), (5*B+4)* (1*A), (4*B+3*C+4)* (1*A), (5*B+3*C+3)* (1*A)])+4]) Asymptotic class: n^2 Time statistics: Partial evaluation computed in 49 ms. Invariants computed in 429 ms. ----Backward Invariants 267 ms. ----Transitive Invariants 32 ms. Refinement performed in 232 ms. Termination proved in 118 ms. Upper bounds computed in 3082 ms. ----Phase cost structures 569 ms. --------Equation cost structures 431 ms. --------Inductive compression(1) 37 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 2478 ms. ----Solving cost expressions 16 ms. Compressed phase information: 17 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 3973 ms.