warning: Ignored call to evalspeedpldi4stop/2 in equation evalspeedpldi4returnin/2 Inferred cost of evalspeedpldi4bb5in(A,B,C,D,E): evalspeedpldi4bb5in(A,B,C,D,E):[[17],[16],18]: 1+it1*(3)+it2*(3) Such that:it1=<1*A+ -1,it1=<1*B+ -2,it1=<1*D+ -1,it1+it2=<1*B,it2=<1*B,it2=<1*B+ -1*A+1,it2=<1*B+ -1*D+1 with precondition: [C=0,E=0,A=D,A>=2,B>=A+1] evalspeedpldi4bb5in(A,B,C,D,E):[[17],18]: 1+it1*(3) Such that:it1=<1*B,it1=<1*B+ -1*A+1,it1=<1*B+ -1*D+1 with precondition: [C=0,E=0,A=D,A>=1,B>=A] Inferred cost of evalspeedpldi4returnin(A,B): evalspeedpldi4returnin(A,B):[20]: 1 with precondition: [] Inferred cost of loop_cont_evalspeedpldi4bb5in(A,B): loop_cont_evalspeedpldi4bb5in(A,B):[22]: 1 with precondition: [] Inferred cost of evalspeedpldi4entryin(A,B): evalspeedpldi4entryin(A,B):[24]: 2 with precondition: [0>=A] evalspeedpldi4entryin(A,B):[25]: 2 with precondition: [A>=B] evalspeedpldi4entryin(A,B):[26]: 3+it1*(3)+it2*(3) Such that:it1=<1*A+ -1,it1=<1*B+ -2,it1+it2=<1*B,it2=<1*B,it2=<1*B+ -1,it2=<1*B+ -1*A+1 with precondition: [A>=2,B>=A+1] evalspeedpldi4entryin(A,B):[27]: 3+it1*(3) Such that:it1=<1*B,it1=<1*B+ -1*A+1 with precondition: [A>=1,B>=A+1] Inferred cost of evalspeedpldi4start(A,B): evalspeedpldi4start(A,B):[29]: 3 with precondition: [0>=A] evalspeedpldi4start(A,B):[30]: 3 with precondition: [A>=B] evalspeedpldi4start(A,B):[31]: 4+it1*(3)+it2*(3) Such that:it1=<1*A+ -1,it1=<1*B+ -2,it1+it2=<1*B,it2=<1*B,it2=<1*B+ -1,it2=<1*B+ -1*A+1 with precondition: [A>=2,B>=A+1] evalspeedpldi4start(A,B):[32]: 4+it1*(3) Such that:it1=<1*B,it1=<1*B+ -1*A+1 with precondition: [A>=1,B>=A+1] Solved cost expressions of evalspeedpldi4start(A,B): evalspeedpldi4start(A,B):[29]: 3 with precondition: [0>=A] evalspeedpldi4start(A,B):[30]: 3 with precondition: [A>=B] evalspeedpldi4start(A,B):[31]: 3*B+4 with precondition: [A>=2,B>=A+1] evalspeedpldi4start(A,B):[32]: -3*A+3*B+7 with precondition: [A>=1,B>=A+1] Maximum cost of evalspeedpldi4start(A,B): max([-3*A+3*B+7,3,3*B+4]) Asymptotic class: n Time statistics: Partial evaluation computed in 6 ms. Invariants computed in 18 ms. ----Backward Invariants 8 ms. ----Transitive Invariants 2 ms. Refinement performed in 17 ms. Termination proved in 5 ms. Upper bounds computed in 47 ms. ----Phase cost structures 13 ms. --------Equation cost structures 13 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 29 ms. ----Solving cost expressions 1 ms. Compressed phase information: 1 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 107 ms.