warning: Ignored call to loop_cont_eval1/3 in equation eval0/3 Inferred cost of eval1(A,B,C,D,E,F,G): eval1(A,B,C,D,E,F,G):[10]: 0 with precondition: [D=1,F=B,G=C,A=E,A>=1] eval1(A,B,C,D,E,F,G):[[8],9,10]: 1+it1*(1) Such that:it1=<1*E+ -1*B,it1=<1*C+ -1*B+ -1,it1=<1*E+1*G+ -1*B with precondition: [D=1,A=E,A+G=F,0>=G+1,A>=1,C>=A+1,G>=B] eval1(A,B,C,D,E,F,G):[[8],10]: 0+it1*(1) Such that:it1=<1*A+ -1*B,it1=<1*E+ -1*B,it1=<1*F+ -1*B,it1=<1*G+ -1*B+ -1 with precondition: [D=1,A=E,C=G,A>=1,C>=A+1,2*A>=F+1,F>=A+B] eval1(A,B,C,D,E,F,G):[9,10]: 1 with precondition: [D=1,B=F,B=A+G,B=E+G,0>=G+1,B>=G+1,C+G>=B+1] Inferred cost of eval0(A,B,C): eval0(A,B,C):[12]: 1 with precondition: [A>=1] eval0(A,B,C):[13]: 2+it1*(1) Such that:it1=<1*A+ -1*B,it1=<-1*B+1*A+ -1,it1=<-1*B+1*C+ -2,it1=<-1*B+1*C+ -1,it1=<1*C+ -1*B+ -1 with precondition: [0>=B+1,A>=1,C>=A+1] eval0(A,B,C):[14]: 1+it1*(1) Such that:it1=<1*A+ -1*B,it1=<-1*B+1*C+ -1,it1=<-1*B+2*A+ -1,it1=<-1*B+2*C+ -3,it1=<1*C+ -1*B+ -1 with precondition: [A>=1,C>=A+1,A>=B+1] eval0(A,B,C):[15]: 2 with precondition: [A>=1,C>=A+1,A>=B+1] Solved cost expressions of eval0(A,B,C): eval0(A,B,C):[12]: 1 with precondition: [A>=1] eval0(A,B,C):[13]: 1*A+ -1*B+1 with precondition: [0>=B+1,A>=1,C>=A+1] eval0(A,B,C):[14]: 1*A+ -1*B+1 with precondition: [A>=1,C>=A+1,A>=B+1] eval0(A,B,C):[15]: 2 with precondition: [A>=1,C>=A+1,A>=B+1] Maximum cost of eval0(A,B,C): max([1*A+ -1*B+1,2]) Asymptotic class: n Time statistics: Partial evaluation computed in 3 ms. Invariants computed in 24 ms. ----Backward Invariants 13 ms. ----Transitive Invariants 1 ms. Refinement performed in 17 ms. Termination proved in 4 ms. Upper bounds computed in 40 ms. ----Phase cost structures 9 ms. --------Equation cost structures 9 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 24 ms. ----Solving cost expressions 2 ms. Compressed phase information: 3 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 100 ms.