warning: Ignored call to evalbinsearchStepSize2stop/9 in equation evalbinsearchStepSize2returnin/9 Inferred cost of evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S): evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[223]: 5 with precondition: [A=0,B=0,C=4,J=0,K=0,L=0,M=4,P=4,R=0,S=4,D=N,G=Q,D>=252,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[226]: 6 with precondition: [A=0,B=0,C=4,J=0,K=0,L=0,M=4,P=4,R=0,S=4,D=N,G=Q,3>=D,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[228]: 4 with precondition: [A=0,B=0,C=4,J=0,K=0,L=0,M=4,P=4,N=D,R=H,S=I,G=O,G=Q] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[230]: 0 with precondition: [A=0,B=0,C=4,J=1,K=0,L=0,M=4,N=D,O=E,P=F,Q=G,R=H,S=I] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,160,229]: 13+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+ -1/4*N+3/4 with precondition: [B=0,C=4,J=0,K=2,L=1,M=1,P=1,R=1,S=1,G=Q,1>=A,255>=N,A>=0,N>=3,O>=G+1,D>=N+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,160,230]: 12+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+1/4*P+ -1/4*N+1/2 with precondition: [B=0,C=4,J=1,K=2,L=1,R=1,M=P,G=Q,M=S,1>=A,1>=M,255>=N,A>=0,2*M>=1,O>=G+1,N>=M+2,D+M>=N+2] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,161,229]: 13+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+ -1/4*N+3/4 with precondition: [B=0,C=4,J=0,K=2,L=1,M=1,P=1,R=1,S=1,G=Q,1>=A,255>=N,A>=0,N>=3,O>=G+1,D>=N+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,161,230]: 12+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+1/4*P+ -1/4*N+1/2 with precondition: [B=0,C=4,J=1,K=2,L=1,R=1,M=P,G=Q,M=S,1>=A,1>=M,255>=N,A>=0,2*M>=1,O>=G+1,N>=M+2,D+M>=N+2] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,164,229]: 14+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+ -1/4*N+1/4 with precondition: [B=0,C=4,J=0,K=1,L=1,M=1,P=1,R=1,S=1,G=Q,1>=A,254>=N,A>=0,N>=1,D>=N+3,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,164,230]: 13+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+ -1/4*N+ -1/4*P+1/2 with precondition: [B=0,C=4,J=1,K=1,L=1,R=1,M=P,G=Q,M=S,1>=A,1>=M,A>=0,2*M>=1,255>=M+N,G>=O+1,M+N>=2,D>=M+N+2] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,216]: 12+it1*(6) Such that:it1=<1/4*D+ -253/4,it1=<1/4*D+ -3/4 with precondition: [B=0,C=4,J=0,K=2,L=1,M=2,N=255,P=1,R=1,S=1,G=Q,1>=A,A>=0,D>=257,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,217]: 12+it1*(6) Such that:it1=<1/4*D+ -253/4,it1=<1/4*D+ -3/4 with precondition: [B=0,C=4,J=0,K=2,L=1,M=2,N=255,P=1,R=1,S=1,G=Q,1>=A,A>=0,D>=257,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,221]: 11+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+ -1/4*N+1/2 with precondition: [B=0,C=4,J=0,K=2,L=1,M=2,R=1,S=2,G=O,G=Q,1>=A,255>=N,1>=P,A>=0,N>=2,2*P>=1,D>=N+2] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],165,230]: 6+it1*(6) Such that:it1=<1/4*D+ -3/4,it1=<1/4*D+1/4*M+ -1/4*N with precondition: [B=0,C=4,J=1,K=2,L=1,P=4,R=1,G=Q,M=S,1>=A,2>=M,255>=N,A>=0,2*M>=3,O>=G+1,N>=M,D+M>=N+4] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],222]: 6+it1*(6) Such that:it1=<1/4*D+ -1/4*N,it1=<1/4*D+ -3/4 with precondition: [B=0,C=4,J=0,K=1,L=0,M=4,P=4,R=1,G=Q,1>=A,2>=S,A>=0,2*S>=3,O>=G+1,D>=N+4,N+S>=256] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],226]: 6+it1*(6) Such that:it1=<1/4*D+ -1/4*N,it1=<1/4*D+ -3/4 with precondition: [B=0,C=4,J=0,K=1,L=0,M=4,P=4,R=0,S=4,G=Q,1>=A,3>=N,A>=0,N>=0,D>=N+4,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],228]: 4+it1*(6) Such that:it1=<1/4*D+ -1/4*N,it1=<1/4*D+ -3/4 with precondition: [B=0,C=4,J=0,K=1,L=0,M=4,P=4,R=0,S=4,G=O,G=Q,1>=A,A>=0,N>=0,D>=N+4] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[[169],230]: 0+it1*(6) Such that:it1=<1/4*D+ -1/4*N,it1=<1/4*D+ -3/4 with precondition: [B=0,C=4,J=1,K=1,L=0,M=4,P=4,R=0,S=4,G=Q,1>=A,A>=0,N>=0,D>=N+4,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,161,229]: 19+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -3/4 with precondition: [A=0,B=0,C=4,J=0,K=2,L=1,M=1,P=1,R=1,S=1,G=Q,254>=N,N>=1,N>=D+7,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,161,230]: 18+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1/4*S+ -1/2 with precondition: [A=0,B=0,C=4,J=1,K=2,L=1,R=1,M=P,G=Q,M=S,1>=M,2*M>=1,O>=G+1,N>=M,M+253>=N,N>=D+M+6] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,162,229]: 20+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1/4 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=1,P=1,R=1,S=1,G=Q,252>=N,N>=0,N>=D+5,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,162,230]: 19+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+1/4*S+ -1/4*D+ -1/2 with precondition: [A=0,B=0,C=4,J=1,K=1,L=1,R=1,M=P,G=Q,M=S,1>=M,N>=0,2*M>=1,253>=M+N,G>=O+1,M+N>=D+6] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,164,229]: 20+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1/4 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=1,P=1,R=1,S=1,G=Q,252>=N,N>=0,N>=D+5,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,164,230]: 19+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+1/4*S+ -1/4*D+ -1/2 with precondition: [A=0,B=0,C=4,J=1,K=1,L=1,R=1,M=P,G=Q,M=S,1>=M,N>=0,2*M>=1,253>=M+N,G>=O+1,M+N>=D+6] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,218]: 19+it1*(5) Such that:it1=<-1/4*D+62,it1=<-1/4*D+ -1/2 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=2,N=0,P=1,R=1,S=1,G=Q,0>=D+6,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,220]: 19+it1*(5) Such that:it1=<-1/4*D+62,it1=<-1/4*D+ -1/2 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=2,N=0,P=1,R=1,S=1,G=Q,0>=D+6,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,221]: 17+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1/2 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=2,R=1,S=2,G=O,G=Q,253>=N,1>=P,N>=0,2*P>=1,N>=D+6] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],168,230]: 12+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+1/4*S+ -1/4*D+ -1 with precondition: [A=0,B=0,C=4,J=1,K=1,L=1,P=4,R=1,G=Q,M=S,2>=M,N>=0,2*M>=3,255>=M+N,G>=O+1,M+N>=D+8] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],224]: 10+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1 with precondition: [A=0,B=0,C=4,J=0,K=2,L=0,M=4,P=4,R=0,S=4,G=Q,255>=N,N>=252,N>=D+8,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],225]: 12+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1 with precondition: [A=0,B=0,C=4,J=0,K=2,L=0,M=4,P=4,R=1,G=Q,2>=S,2*S>=3,N>=D+8,S>=N+1,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],228]: 9+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1 with precondition: [A=0,B=0,C=4,J=0,K=2,L=0,M=4,P=4,R=0,S=4,G=O,G=Q,255>=N,N>=D+8] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,[167],230]: 5+it1*(5) Such that:it1=<-1/4*D+62,it1=<1/4*N+ -1/4*D+ -1 with precondition: [A=0,B=0,C=4,J=1,K=2,L=0,M=4,P=4,R=0,S=4,G=Q,255>=N,N>=D+8,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,161,229]: 19 with precondition: [A=0,B=0,C=4,J=0,K=2,L=1,M=1,P=1,R=1,S=1,N=D+3,G=Q,254>=N,N>=1,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,161,230]: 18 with precondition: [A=0,B=0,C=4,J=1,K=2,L=1,R=1,M=P,G=Q,M=S,D+M+2=N,1>=M,2*M>=1,O>=G+1,N>=M,M+253>=N] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,162,229]: 20 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=1,P=1,R=1,S=1,N=D+1,G=Q,252>=N,N>=0,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,162,230]: 19 with precondition: [A=0,B=0,C=4,J=1,K=1,L=1,R=1,M=P,G=Q,M=S,M+N=D+2,251>=D,1>=M,2*M>=1,D+2>=M,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,164,229]: 20 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=1,P=1,R=1,S=1,N=D+1,G=Q,252>=N,N>=0,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,164,230]: 19 with precondition: [A=0,B=0,C=4,J=1,K=1,L=1,R=1,M=P,G=Q,M=S,M+N=D+2,251>=D,1>=M,2*M>=1,D+2>=M,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,218]: 19 with precondition: [A=0,B=0,C=4,D+2=0,J=0,K=1,L=1,M=2,N=0,P=1,R=1,S=1,G=Q,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,220]: 19 with precondition: [A=0,B=0,C=4,D+2=0,J=0,K=1,L=1,M=2,N=0,P=1,R=1,S=1,G=Q,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,221]: 17 with precondition: [A=0,B=0,C=4,J=0,K=1,L=1,M=2,R=1,S=2,N=D+2,G=O,G=Q,253>=N,1>=P,N>=0,2*P>=1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,168,230]: 12 with precondition: [A=0,B=0,C=4,J=1,K=1,L=1,P=4,R=1,G=Q,M=S,M+N=D+4,251>=D,2>=M,2*M>=3,D+4>=M,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,224]: 10 with precondition: [A=0,B=0,C=4,J=0,K=2,L=0,M=4,P=4,R=0,S=4,N=D+4,G=Q,255>=N,N>=252,O>=G+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,225]: 12 with precondition: [A=0,B=0,C=4,J=0,K=2,L=0,M=4,P=4,R=1,N=D+4,G=Q,2>=S,2*S>=3,S>=N+1,G>=O+1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,228]: 9 with precondition: [A=0,B=0,C=4,J=0,K=2,L=0,M=4,P=4,R=0,S=4,N=D+4,G=O,G=Q,255>=N] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S):[166,230]: 5 with precondition: [A=0,B=0,C=4,J=1,K=2,L=0,M=4,P=4,R=0,S=4,N=D+4,G=Q,255>=N,O>=G+1] Inferred cost of evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I): evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I):[232]: 1 with precondition: [] Inferred cost of loop_cont_evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I): loop_cont_evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I):[234]: 1 with precondition: [] Inferred cost of evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I): evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[236]: 7 with precondition: [A>=252] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[237]: 8 with precondition: [3>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[238]: 6 with precondition: [] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[239]: 15+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[240]: 15+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[241]: 16+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[242]: 14+it1*(6) Such that:it1=<1/4*A+ -253/4,it1=<1/4*A+ -3/4 with precondition: [A>=257] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[243]: 14+it1*(6) Such that:it1=<1/4*A+ -253/4,it1=<1/4*A+ -3/4 with precondition: [A>=257] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[244]: 13+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[245]: 8+it1*(6) Such that:it1=<1/4*A+ -127/2,it1=<1/4*A+ -3/4 with precondition: [A>=258] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[246]: 8+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[247]: 6+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[248]: 21+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[249]: 22+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[250]: 22+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[251]: 21+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+ -1/2 with precondition: [0>=A+6] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[252]: 21+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+ -1/2 with precondition: [0>=A+6] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[253]: 19+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[254]: 12+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[255]: 14+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+ -3/4 with precondition: [0>=A+7] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[256]: 11+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[257]: 21 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[258]: 22 with precondition: [251>=A,A+1>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[259]: 22 with precondition: [251>=A,A+1>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[260]: 21 with precondition: [A+2=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[261]: 21 with precondition: [A+2=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[262]: 19 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[263]: 12 with precondition: [251>=A,A>=248] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[264]: 14 with precondition: [0>=A+3] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[265]: 11 with precondition: [251>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[266]: 1 with precondition: [] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[267]: 13+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[268]: 13+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[269]: 14+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[270]: 7+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[271]: 1+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[272]: 19+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[273]: 20+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[274]: 20+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[275]: 13+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[276]: 6+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[277]: 19 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[278]: 20 with precondition: [251>=A,2*A+3>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[279]: 20 with precondition: [251>=A,2*A+3>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[280]: 13 with precondition: [251>=A,2*A+5>=0] evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I):[281]: 6 with precondition: [251>=A] Inferred cost of evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I): evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[283]: 8 with precondition: [A>=252] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[284]: 9 with precondition: [3>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[285]: 7 with precondition: [] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[286]: 16+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[287]: 16+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[288]: 17+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[289]: 15+it1*(6) Such that:it1=<1/4*A+ -253/4,it1=<1/4*A+ -3/4 with precondition: [A>=257] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[290]: 15+it1*(6) Such that:it1=<1/4*A+ -253/4,it1=<1/4*A+ -3/4 with precondition: [A>=257] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[291]: 14+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[292]: 9+it1*(6) Such that:it1=<1/4*A+ -127/2,it1=<1/4*A+ -3/4 with precondition: [A>=258] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[293]: 9+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[294]: 7+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[295]: 22+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[296]: 23+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[297]: 23+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[298]: 22+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+ -1/2 with precondition: [0>=A+6] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[299]: 22+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+ -1/2 with precondition: [0>=A+6] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[300]: 20+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[301]: 13+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[302]: 15+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+ -3/4 with precondition: [0>=A+7] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[303]: 12+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[304]: 22 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[305]: 23 with precondition: [251>=A,A+1>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[306]: 23 with precondition: [251>=A,A+1>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[307]: 22 with precondition: [A+2=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[308]: 22 with precondition: [A+2=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[309]: 20 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[310]: 13 with precondition: [251>=A,A>=248] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[311]: 15 with precondition: [0>=A+3] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[312]: 12 with precondition: [251>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[313]: 2 with precondition: [] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[314]: 14+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[315]: 14+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[316]: 15+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[317]: 8+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[318]: 2+it1*(6) Such that:it1=<1/4*A,it1=<1/4*A+ -3/4 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[319]: 20+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[320]: 21+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[321]: 21+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[322]: 14+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[323]: 7+it1*(5) Such that:it1=<-1/4*A+62,it1=<-1/4*A+251/4 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[324]: 20 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[325]: 21 with precondition: [251>=A,2*A+3>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[326]: 21 with precondition: [251>=A,2*A+3>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[327]: 14 with precondition: [251>=A,2*A+5>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[328]: 7 with precondition: [251>=A] Solved cost expressions of evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I): evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[283]: 8 with precondition: [A>=252] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[284]: 9 with precondition: [3>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[285]: 7 with precondition: [] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[286]: 3/2*A+23/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[287]: 3/2*A+23/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[288]: 3/2*A+25/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[289]: 3/2*A+ -729/2 with precondition: [A>=257] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[290]: 3/2*A+ -729/2 with precondition: [A>=257] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[291]: 3/2*A+19/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[292]: 3/2*A+ -372 with precondition: [A>=258] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[293]: 3/2*A+9/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[294]: 3/2*A+5/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[295]: -5/4*A+332 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[296]: -5/4*A+333 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[297]: -5/4*A+333 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[298]: -5/4*A+39/2 with precondition: [0>=A+6] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[299]: -5/4*A+39/2 with precondition: [0>=A+6] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[300]: -5/4*A+330 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[301]: -5/4*A+323 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[302]: -5/4*A+45/4 with precondition: [0>=A+7] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[303]: -5/4*A+322 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[304]: 22 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[305]: 23 with precondition: [251>=A,A+1>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[306]: 23 with precondition: [251>=A,A+1>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[307]: 22 with precondition: [A+2=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[308]: 22 with precondition: [A+2=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[309]: 20 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[310]: 13 with precondition: [251>=A,A>=248] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[311]: 15 with precondition: [0>=A+3] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[312]: 12 with precondition: [251>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[313]: 2 with precondition: [] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[314]: 3/2*A+19/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[315]: 3/2*A+19/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[316]: 3/2*A+21/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[317]: 3/2*A+7/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[318]: 3/2*A+ -5/2 with precondition: [A>=4] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[319]: -5/4*A+330 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[320]: -5/4*A+331 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[321]: -5/4*A+331 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[322]: -5/4*A+324 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[323]: -5/4*A+317 with precondition: [247>=A] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[324]: 20 with precondition: [251>=A,A+2>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[325]: 21 with precondition: [251>=A,2*A+3>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[326]: 21 with precondition: [251>=A,2*A+3>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[327]: 14 with precondition: [251>=A,2*A+5>=0] evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I):[328]: 7 with precondition: [251>=A] Maximum cost of evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I): max([3/2*A+25/2,-5/4*A+333,23]) Asymptotic class: n Time statistics: Partial evaluation computed in 723 ms. Invariants computed in 917 ms. ----Backward Invariants 551 ms. ----Transitive Invariants 10 ms. Refinement performed in 4247 ms. Termination proved in 26 ms. Upper bounds computed in 1157 ms. ----Phase cost structures 145 ms. --------Equation cost structures 131 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 956 ms. ----Solving cost expressions 11 ms. Compressed phase information: 111 Compressed Chains: 0 Compressed invariants: 10 Total analysis performed in 7575 ms.