warning: Ignored call to loop_cont_a/1 in equation start/1 warning: Ignored call to loop_cont_a/1 in equation start/1 Inferred cost of a(A,B,C): a(A,B,C):[10]: 0 with precondition: [B=1,A=C,A>=1] a(A,B,C):[[9],10]: 0+it1*(1) Such that:it1=<1*A,it1=<1*A+ -1*C with precondition: [B=1,C>=0,A>=C+1] Inferred cost of start(A): start(A):[12]: 1 with precondition: [A>=1] start(A):[13]: 1+it1*(1) Such that:it1=<1*A with precondition: [A>=1] start(A):[14]: 1 with precondition: [A=100] start(A):[15]: 1+it1*(1) Such that:it1=<100 with precondition: [A=100] Solved cost expressions of start(A): start(A):[12]: 1 with precondition: [A>=1] start(A):[13]: 1*A+1 with precondition: [A>=1] start(A):[14]: 1 with precondition: [A=100] start(A):[15]: 101 with precondition: [A=100] Maximum cost of start(A): max([1*A+1,101]) Asymptotic class: n Time statistics: Partial evaluation computed in 2 ms. Invariants computed in 5 ms. ----Backward Invariants 3 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.