warning: Ignored call to evaleasy2stop/1 in equation evaleasy2returnin/1 Inferred cost of evaleasy2bb1in(A,B,C): evaleasy2bb1in(A,B,C):[14]: 1 with precondition: [B=0,A=C,0>=A] evaleasy2bb1in(A,B,C):[[13],14]: 1+it1*(2) Such that:it1=<1*A with precondition: [B=0,C=0,A>=1] Inferred cost of evaleasy2returnin(A): evaleasy2returnin(A):[16]: 1 with precondition: [] Inferred cost of loop_cont_evaleasy2bb1in(A): loop_cont_evaleasy2bb1in(A):[18]: 1 with precondition: [] Inferred cost of evaleasy2entryin(A): evaleasy2entryin(A):[20]: 3 with precondition: [0>=A] evaleasy2entryin(A):[21]: 3+it1*(2) Such that:it1=<1*A with precondition: [A>=1] Inferred cost of evaleasy2start(A): evaleasy2start(A):[23]: 4 with precondition: [0>=A] evaleasy2start(A):[24]: 4+it1*(2) Such that:it1=<1*A with precondition: [A>=1] Solved cost expressions of evaleasy2start(A): evaleasy2start(A):[23]: 4 with precondition: [0>=A] evaleasy2start(A):[24]: 2*A+4 with precondition: [A>=1] Maximum cost of evaleasy2start(A): max([2*A+4,4]) Asymptotic class: n Time statistics: Partial evaluation computed in 2 ms. Invariants computed in 4 ms. ----Backward Invariants 2 ms. ----Transitive Invariants 1 ms. Refinement performed in 6 ms. Termination proved in 1 ms. Upper bounds computed in 9 ms. ----Phase cost structures 3 ms. --------Equation cost structures 3 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 3 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 29 ms.