warning: Ignored call to evalgcdstop/2 in equation evalgcdreturnin/2 Inferred cost of evalgcdbb7in(A,B,C,D,E): evalgcdbb7in(A,B,C,D,E):[19]: 1 with precondition: [C=0,B=A,B=D,B=E,B>=1] evalgcdbb7in(A,B,C,D,E):[20]: 0 with precondition: [C=1,A=D,B=E,A>=1,B>=1] evalgcdbb7in(A,B,C,D,E):[[17,18],19]: 1+it1*(3)+it2*(3) Such that:it1=<1*A+ -1,it1=<1*A+ -1*E,it1+it2=<1*A+1*B+ -2,it1+it2=<1*A+1*B+ -2*D,it2=<1*B+ -1,it2=<1*B+ -1*E with precondition: [C=0,D=E,D>=1,A>=D,B>=D,A+B>=3*D] evalgcdbb7in(A,B,C,D,E):[[17,18],20]: 0+it1*(3)+it2*(3) Such that:it1=<1*A+ -1,it1=<1*A+ -1*D,it1+it2=<1*A+1*B+ -2,it1+it2=<1*A+1*B+ -1*D+ -1*E,it2=<1*B+ -1,it2=<1*B+ -1*E with precondition: [C=1,D>=1,E>=1,A>=D,B>=E,A+B>=D+E+1] Inferred cost of evalgcdreturnin(A,B): evalgcdreturnin(A,B):[22]: 1 with precondition: [] Inferred cost of loop_cont_evalgcdbb7in(A,B): loop_cont_evalgcdbb7in(A,B):[24]: 1 with precondition: [] Inferred cost of evalgcdentryin(A,B): evalgcdentryin(A,B):[26]: 2 with precondition: [0>=A] evalgcdentryin(A,B):[27]: 2 with precondition: [0>=B] evalgcdentryin(A,B):[28]: 3 with precondition: [A=B,A>=1] evalgcdentryin(A,B):[29]: 3+it1*(3)+it2*(3) Such that:it1=<1*B+ -1,it1+it2=<1*A+1*B+ -2,it2=<1*A+ -1 with precondition: [A>=1,B>=1,A+B>=3] evalgcdentryin(A,B):[30]: 1 with precondition: [A>=1,B>=1] evalgcdentryin(A,B):[31]: 1+it1*(3)+it2*(3) Such that:it1=<1*B+ -1,it1+it2=<1*A+1*B+ -2,it2=<1*A+ -1 with precondition: [A>=1,B>=1,A+B>=3] Inferred cost of evalgcdstart(A,B): evalgcdstart(A,B):[33]: 3 with precondition: [0>=A] evalgcdstart(A,B):[34]: 3 with precondition: [0>=B] evalgcdstart(A,B):[35]: 4 with precondition: [A=B,A>=1] evalgcdstart(A,B):[36]: 4+it1*(3)+it2*(3) Such that:it1=<1*B+ -1,it1+it2=<1*A+1*B+ -2,it2=<1*A+ -1 with precondition: [A>=1,B>=1,A+B>=3] evalgcdstart(A,B):[37]: 2 with precondition: [A>=1,B>=1] evalgcdstart(A,B):[38]: 2+it1*(3)+it2*(3) Such that:it1=<1*B+ -1,it1+it2=<1*A+1*B+ -2,it2=<1*A+ -1 with precondition: [A>=1,B>=1,A+B>=3] Solved cost expressions of evalgcdstart(A,B): evalgcdstart(A,B):[33]: 3 with precondition: [0>=A] evalgcdstart(A,B):[34]: 3 with precondition: [0>=B] evalgcdstart(A,B):[35]: 4 with precondition: [A=B,A>=1] evalgcdstart(A,B):[36]: 3*A+3*B+ -2 with precondition: [A>=1,B>=1,A+B>=3] evalgcdstart(A,B):[37]: 2 with precondition: [A>=1,B>=1] evalgcdstart(A,B):[38]: 3*A+3*B+ -4 with precondition: [A>=1,B>=1,A+B>=3] Maximum cost of evalgcdstart(A,B): max([3*A+3*B+ -2,4]) Asymptotic class: n Time statistics: Partial evaluation computed in 6 ms. Invariants computed in 18 ms. ----Backward Invariants 11 ms. ----Transitive Invariants 2 ms. Refinement performed in 19 ms. Termination proved in 7 ms. Upper bounds computed in 46 ms. ----Phase cost structures 19 ms. --------Equation cost structures 14 ms. --------Inductive compression(1) 1 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 20 ms. ----Solving cost expressions 1 ms. Compressed phase information: 3 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 109 ms.